update comment in configure about installdirs var field

SkySkimmer · Jan 14, 2025 · 5735809 · 5735809
1 parent 32db14e
commit 5735809
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/tools/configure/configure.ml b/tools/configure/configure.ml
@@ -210,7 +210,7 @@ module InstallDir = struct
 
   type t =
     { var : string
-    (** Makefile variable to write *)
+    (** Used as key by [select] (otherwise ignored) *)
     ; msg : string
     (** Description of the directory  *)
     ; uservalue : string option