diff options
Diffstat (limited to 'camlp4/tools/camlp4_comm.sh')
| -rwxr-xr-x | camlp4/tools/camlp4_comm.sh | 38 |
1 files changed, 0 insertions, 38 deletions
diff --git a/camlp4/tools/camlp4_comm.sh b/camlp4/tools/camlp4_comm.sh deleted file mode 100755 index b6bb8f87ed..0000000000 --- a/camlp4/tools/camlp4_comm.sh +++ /dev/null @@ -1,38 +0,0 @@ -#!/bin/sh -# $Id$ - -ARGS1= -FILE= -QUIET=no -while test "" != "$1"; do - case $1 in - -q) QUIET=yes;; - *.ml*) FILE=$1;; - *) ARGS1="$ARGS1 $1";; - esac - shift -done - -# FILE must exist and be non empty (at least one line) -test -s "$FILE" || exit 1 - -set - `awk 'NR == 1' "$FILE"` -if test "$2" = "camlp4r" -o "$2" = "camlp4"; then - COMM="ocamlrun$EXE ../boot/$2$EXE -nolib -I ../boot" - if test "`basename $OTOP`" != "ocaml_stuff"; then - COMM="$OTOP/boot/$COMM" - fi - shift; shift - ARGS2=`echo $* | sed -e "s/[()*]//g"` -# ARGS1="$ARGS1 -verbose" - if test "$QUIET" = "no"; then echo $COMM $ARGS2 $ARGS1 $FILE; fi - $COMM $ARGS2 $ARGS1 $FILE -else - if test "`basename $FILE .mli`.mli" = "$FILE"; then - OFILE=`basename $FILE .mli`.ppi - else - OFILE=`basename $FILE .ml`.ppo - fi - if test "$QUIET" = "no"; then echo cp $FILE $OFILE; fi - cp $FILE $OFILE -fi |