diff options
-rwxr-xr-x | camlp4/etc/mkcamlp4.sh.tpl | 9 |
1 files changed, 9 insertions, 0 deletions
diff --git a/camlp4/etc/mkcamlp4.sh.tpl b/camlp4/etc/mkcamlp4.sh.tpl index 00ae41fbd..649399833 100755 --- a/camlp4/etc/mkcamlp4.sh.tpl +++ b/camlp4/etc/mkcamlp4.sh.tpl @@ -22,3 +22,12 @@ while test "" != "$1"; do esac shift done + +CRC=crc_$$ +set -e +trap 'rm -f $CRC.ml $CRC.cmi $CRC.cmo' 0 2 +$OLIB/extract_crc -I $OLIB $INCL $INTERFACES > $CRC.ml +echo "let _ = Dynlink.add_available_units crc_unit_list" >> $CRC.ml +ocamlc -I $LIB odyl.cma camlp4.cma $CRC.ml $INCL $OPTS odyl.cmo -linkall +rm -f $CRC.ml $CRC.cmi $CRC.cmo + |