Fix include Bignum failure when hol.sh is loaded outside hol-light

jrh13 · Aug 8, 2024 · ebaefd1 · ebaefd1
1 parent 7f7808d
commit ebaefd1
Show file tree

Hide file tree

Showing 2 changed files with 2 additions and 2 deletions.
diff --git a/hol_4.14.sh b/hol_4.14.sh
@@ -15,4 +15,4 @@ if [ -d "${HOLLIGHT_DIR}/_opam" ]; then
   eval $(opam env --switch "${HOLLIGHT_DIR}/" --set-switch)
 fi
 
-${LINE_EDITOR} ${HOLLIGHT_DIR}/ocaml-hol -init ${HOLLIGHT_DIR}/hol.ml
+${LINE_EDITOR} ${HOLLIGHT_DIR}/ocaml-hol -init ${HOLLIGHT_DIR}/hol.ml -I ${HOLLIGHT_DIR}
diff --git a/hol_4.sh b/hol_4.sh
@@ -15,4 +15,4 @@ if [ -d "${HOLLIGHT_DIR}/_opam" ]; then
   eval $(opam env --switch "${HOLLIGHT_DIR}/" --set-switch)
 fi
 
-${LINE_EDITOR} ${HOLLIGHT_DIR}/ocaml-hol -I `camlp5 -where` camlp5o.cma -init ${HOLLIGHT_DIR}/hol.ml -safe-string
+${LINE_EDITOR} ${HOLLIGHT_DIR}/ocaml-hol -I `camlp5 -where` camlp5o.cma -init ${HOLLIGHT_DIR}/hol.ml -safe-string -I ${HOLLIGHT_DIR}