Filenames

A filename is any sequence of nonblank characters enclosed by spaces. In particular, the filename may contain one-character words, and it is case sensitive. This deviation from the general definitions of words and strings is done in order to allow for machine-specific filename specifications without having to enclose the filename in quotes.

Subsections

Xplor-NIH 2023-11-10