NOFRAGMENT = 'nofragment'
NOINDENT = 'noindent'
NOQUOTE = 'noquote'
+NORAGGED_RIGHT = 'noragged-right'
NOTES = 'body'
NOTIME = 'notime'
OUTPUT = 'output'
RAGGED_RIGHT: r'''ragged-right = ##t''',
+ NORAGGED_RIGHT: r'''ragged-right = ##f''',
+
PACKED: r'''packed = ##t''',
},
if 'ddump-profile' in global_options.process_cmd:
require_file (base + '.profile')
+ if 'dseparate-log-file' in global_options.process_cmd:
+ require_file (base + '.log')
map (consider_file, [base + '.tex',
base + '.eps',