summaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
-rwxr-xr-xcamlp4/etc/mkcamlp4.sh.tpl9
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
+