Provide a smidgeon of in-file documentation for parse_glob

HOL-Theorem-Prover · Oct 27, 2014 · 7da4c56 · 7da4c56
1 parent 8308dd1
commit 7da4c56
Showing 1 changed file with 9 additions and 0 deletions.
diff --git a/tools/Holmake/parse_glob.sig b/tools/Holmake/parse_glob.sig
@@ -4,3 +4,12 @@ sig
   val parse_glob : string -> regexpMatch.regexp
 
 end
+
+(* [parse_glob s] returns the regular expression corresponding to the
+   shell glob-expression s. Glob-expressions use the ?, [ and *
+   meta-characters and are documented in shell manual pages.
+
+   All strings generate a regular expression in this syntax. For
+   example, the superficially malformed "[a-" is the regular expression
+   that matches the one string "[a-".
+*)