Fix hol-mode.sml references broken by 73921f8

HOL-Theorem-Prover · Oct 3, 2024 · d17a401 · d17a401
1 parent 73921f8
commit d17a401
Show file tree

Hide file tree

Showing 2 changed files with 2 additions and 2 deletions.
diff --git a/examples/separationLogic/src/holfoot/poly/build-state.hol b/examples/separationLogic/src/holfoot/poly/build-state.hol
@@ -13,7 +13,7 @@ open holfootLib;
 
 open separationLogicTheory vars_as_resourceTheory holfootTheory generalHelpersTheory;
 
-use (Globals.HOLDIR ^ "/tools/hol-mode.sml");
+use (Globals.HOLDIR ^ "/tools/editor-modes/emacs/hol-mode.sml");
 
 val _ = Feedback.set_trace "Unicode" 0;
 val _ = Feedback.set_trace "PPBackEnd use annotations" 0;

diff --git a/tools/editor-modes/emacs/hol-mode.src b/tools/editor-modes/emacs/hol-mode.src
@@ -69,7 +69,7 @@ a new buffer that is vertically adjacent and below)."
   (setq holmake-executable filename))
 
 (defvar hol-mode-sml-init-command
-   "use (Globals.HOLDIR ^ \"/tools/editors-modes/emacs/hol-mode.sml\")"
+   "use (Globals.HOLDIR ^ \"/tools/editor-modes/emacs/hol-mode.sml\")"
   "*The command to send to HOL to load the ML-part of hol-mode.")