-- WriteString.config
-- written by Hilton, August 4, 1982 1:42 PM
-- last modified by McCreight, March 23, 1983 11:04 AM


WriteString: CONFIGURATION
IMPORTS ChipUserInt, ppdddefs, ppddefs,
ppdefs, ppfeeddefs, String
EXPORTS WriteStringDefs
CONTROL DebugWriteString =

BEGIN
DebugWriteString;
WriteStringImpl;
END. -- of WriteString --