blob: 64a4e2b1d3e94886b1c88e62ee5d22410855f7a8 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
|
#!/bin/sh
DIR=`expr "$0" : "\(.*\)/.*" "|" "."`
INCL=
FILE=
while test "" != "$1"; do
case $1 in
-I) INCL="$INCL -I $2"; shift;;
*) FILE=$1;;
esac
shift
done
set - `awk 'NR == 1' "$FILE"`
if test "$2" = "camlp4r" -o "$2" = "camlp4"; then
COMM="$OTOP/boot/ocamlrun $DIR/../boot/$2 -nolib -I $DIR/../boot $INCL $DIR/../etc/pr_o.cmo"
shift; shift
ARGS=`echo $* | sed -e "s/[()*]//g"`
$COMM $ARGS -ss $FILE
else
cat $FILE
fi
|
