diff options
Diffstat (limited to 'configure.gnu')
| -rwxr-xr-x | configure.gnu | 7 |
1 files changed, 0 insertions, 7 deletions
diff --git a/configure.gnu b/configure.gnu deleted file mode 100755 index 925dc44..0000000 --- a/configure.gnu +++ /dev/null @@ -1,7 +0,0 @@ -#!/bin/sh - -par="--without-arts" - -echo "*** Doing configure $* $par ..." - -./configure $* $par
\ No newline at end of file |