/usr/share/hol88-2.02.19940316/help/ENTRIES/help.doc is in hol88-help 2.02.19940316-35.
This file is owned by root:root, with mode 0o644.
The actual contents of the file can be viewed below.
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 | \DOC help
\TYPE {help : (string -> void)}
\SYNOPSIS
Displays help on a given identifier in the system.
\DESCRIBE
{help} will attempt to display the help file associated with a particular
identifier in the system. The identifier is provided as an ML string, and
the file should be located somewhere on the help search path. Normally the help
file for an identifier {name} would be called {name.doc}, but there are a few
exceptions, because some identifiers have characters that cannot be put in
filenames (e.g. `{/}' under Unix, which is the directory separator).
\FAILURE
Fails if no information can be found on the identifier in question.
\SEEALSO
help_search_path, set_help_search_path.
\ENDDOC
|