diff --git a/hol_4.14.sh b/hol_4.14.sh index 95bc44ae..c81fb3e6 100755 --- 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 index a475fe5d..ef8dec4c 100755 --- 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}