hol_expand_directory : string -> string
Modifies directory name starting with $ to include HOL directory
The function hol_expand_directory takes a string indicating a directory. If
it does not begin with a dollar sign $, the string is returned unchanged.
Otherwise, the initial dollar sign is replaced with the current HOL Light
directory hol_dir. To get an actual $ at the start of the returned
directory, actually use two dollar signs $$.
- FAILURE CONDITIONS
val it : string ref = contents = "/home/johnh/holl"
# hol_expand_directory "$/Help";;
val it : string = "/home/johnh/holl/Help"
- SEE ALSO
file_on_path, help_path, load_on_path, load_path.