diff options
Diffstat (limited to 'etc/bigloo/autoconf/bfildir')
| -rwxr-xr-x | etc/bigloo/autoconf/bfildir | 36 |
1 files changed, 0 insertions, 36 deletions
diff --git a/etc/bigloo/autoconf/bfildir b/etc/bigloo/autoconf/bfildir deleted file mode 100755 index 128d5c7..0000000 --- a/etc/bigloo/autoconf/bfildir +++ /dev/null @@ -1,36 +0,0 @@ -#!/bin/sh -#*=====================================================================*/ -#* serrano/prgm/project/scribe/autoconf/bfildir */ -#* ------------------------------------------------------------- */ -#* Author : Manuel Serrano */ -#* Creation : Tue Jan 12 14:53:33 1999 */ -#* Last change : Wed Aug 7 21:41:06 2002 (serrano) */ -#* ------------------------------------------------------------- */ -#* Find out the directory where Bigloo is installed */ -#*=====================================================================*/ -bigloo=bigloo - -#*---------------------------------------------------------------------*/ -#* We parse the arguments */ -#*---------------------------------------------------------------------*/ -while : ; do - case $1 in - "") - break;; - --bigloo=*|-bigloo=*) - bigloo="`echo $1 | sed 's/^[-a-z]*=//'`";; - - -*) - echo "Unknown option \"$1\", ignored" >&2;; - esac - shift -done - -#*---------------------------------------------------------------------*/ -#* We spawn a bigloo process to check its version number */ -#*---------------------------------------------------------------------*/ -$bigloo -q -eval "(begin (print *default-lib-dir*) (exit 0))" - -exit 0 - - |