diff options
Diffstat (limited to 'camlp4/meta/mk_q_MLast.sh')
| -rwxr-xr-x | camlp4/meta/mk_q_MLast.sh | 12 |
1 files changed, 0 insertions, 12 deletions
diff --git a/camlp4/meta/mk_q_MLast.sh b/camlp4/meta/mk_q_MLast.sh deleted file mode 100755 index c678f350ad..0000000000 --- a/camlp4/meta/mk_q_MLast.sh +++ /dev/null @@ -1,12 +0,0 @@ -#!/bin/sh -# $Id$ - -IFILE=pa_r.ml -OFILE=q_MLast.ml -( -sed -e '/^EXTEND$/,$d' $OFILE -echo EXTEND -../../boot/ocamlrun ./camlp4r -I . -I ../etc q_MLast.cmo pa_extend.cmo pr_r.cmo pr_extend.cmo -cip -quotify $IFILE | sed -e '1,/^EXTEND$/d' -e '/^END;$/,$d' -echo ' (* Antiquotations for local entries *)' -sed -e '1,/Antiquotations for local entries/d' $OFILE -) |