From 71f1a9fd6bf04cfc7ddfe62311e5d1b010f75e92 Mon Sep 17 00:00:00 2001 From: Michael Norrish Date: Tue, 17 Dec 2024 17:51:20 +1100 Subject: [PATCH] Document internal Holmake function in a comment --- tools/Holmake/Holmake.sml | 7 +++++++ 1 file changed, 7 insertions(+) diff --git a/tools/Holmake/Holmake.sml b/tools/Holmake/Holmake.sml index b45ef318d8..115451de29 100644 --- 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())