Document internal Holmake function in a comment

HOL-Theorem-Prover · Dec 17, 2024 · 71f1a9f · 71f1a9f
1 parent 02d5170
commit 71f1a9f
Showing 1 changed file with 7 additions and 0 deletions.
diff --git a/tools/Holmake/Holmake.sml b/tools/Holmake/Holmake.sml
@@ -196,6 +196,13 @@ fun extend_with_cline_vars env =
     end
 
 
+(* ----------------------------------------------------------------------
+    get_hmf : unit -> "holmakefile data" (as per ReadHMF)
+
+    Utility function to get the Holmakefile in the current directory, but
+    using a cache so that any given file is only ever read once.
+   ---------------------------------------------------------------------- *)
+
 local
   open hm_target
   val base = extend_with_cline_vars (read_holpathdb())