gui: Mark print_startup_time() unused to avoid warning.
[pspp] / doc / dev / syntax.texi
2007-11-11 Ben PfaffPatch #6262. New developers guide and resulting fixes...