// for SHORT_FILENAME
// mgplot();	// load "mgplot.mm"
mgplot_quit();