Merge pull request #106 from aqjune-aws/bugfix

Fix include Bignum failure when hol.sh is loaded outside hol-light
jrh13 · Aug 8, 2024 · 016d226 · 016d226
2 parents 7f7808d + ebaefd1
commit 016d226
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}