Revision 07fc868ecfd31fecc7c3f964730f946c31f5ab80 authored by Joshua J. Cogliati on 19 June 2020, 15:11:03 UTC, committed by Joshua J. Cogliati on 19 June 2020, 15:11:03 UTC
1 parent ecd99ed
erasefile
ERASEFILE filename
ERF filename
command. Erases (deletes, removes) the named file, which should not
currently be open.
Computing file changes ...