PATCH-FILE : FLAG

PATCH-FILE is a flag or parameter.
Name of the file containing changes to the grader core image.
PATCH-FILE takes values of type FILESPEC.
It belongs to subjects GR-FILENAMES .
Its default value is "grader.patch"
Its current value is "grader.patch".

TPS documentation homepage


© 1988-99, Carnegie Mellon University.

TPS homepage