From d17a401e2498135454cb1229c814b1e55fd26433 Mon Sep 17 00:00:00 2001 From: Michael Norrish Date: Thu, 3 Oct 2024 15:31:23 +1000 Subject: [PATCH] Fix hol-mode.sml references broken by 73921f89dd6 --- examples/separationLogic/src/holfoot/poly/build-state.hol | 2 +- tools/editor-modes/emacs/hol-mode.src | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/examples/separationLogic/src/holfoot/poly/build-state.hol b/examples/separationLogic/src/holfoot/poly/build-state.hol index bec2deaba0..030286f574 100644 --- 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 index c8e250ed4c..35197f5c80 100644 --- 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.")