diff options
Diffstat (limited to 'newlib/doc/makedocbook.py')
| -rwxr-xr-x | newlib/doc/makedocbook.py | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/newlib/doc/makedocbook.py b/newlib/doc/makedocbook.py index 1b4f5ab33..0c84e3c47 100755 --- a/newlib/doc/makedocbook.py +++ b/newlib/doc/makedocbook.py @@ -824,8 +824,12 @@ def main(file): if __name__ == '__main__' : options = OptionParser() options.add_option('-v', '--verbose', action='count', dest = 'verbose') + options.add_option('-c', '--cache', action='store_true', dest = 'cache', help="just ensure PLY cache is up to date") (opts, args) = options.parse_args() + if opts.cache: + sys.exit() + verbose = opts.verbose if len(args) > 0: |