[emacs-mode] Modify holmake command to emit message to minibuffer

HOL-Theorem-Prover · Feb 13, 2024 · 14e9458 · 14e9458
1 parent cc20395
commit 14e9458
Showing 1 changed file with 1 addition and 0 deletions.
diff --git a/tools/hol-mode.src b/tools/hol-mode.src
@@ -874,6 +874,7 @@ region instead. With prefix ARG prompt for a file-name to load."
     (setq buffer-read-only nil)
     (delete-region (point-min) (point-max))
     (insert "Running Holmake in directory " dir "\n\n")
+    (message "Running Holmake in directory %s" dir)
     (term-ansi-make-term
      (buffer-name)
      holmake-executable nil "--qof" "-k")