diff options
Diffstat (limited to 'Tools/webchecker/webchecker.py')
-rwxr-xr-x | Tools/webchecker/webchecker.py | 32 |
1 files changed, 18 insertions, 14 deletions
diff --git a/Tools/webchecker/webchecker.py b/Tools/webchecker/webchecker.py index 5459e97..bf56cec 100755 --- a/Tools/webchecker/webchecker.py +++ b/Tools/webchecker/webchecker.py @@ -183,24 +183,28 @@ def main(): for arg in args: c.addroot(arg) - if not norun: + try: + + if not norun: + try: + c.run() + except KeyboardInterrupt: + if verbose > 0: + print "[run interrupted]" + try: - c.run() + c.report() except KeyboardInterrupt: if verbose > 0: - print "[run interrupted]" + print "[report interrupted]" - try: - c.report() - except KeyboardInterrupt: - if verbose > 0: - print "[report interrupted]" - - if c.save_pickle(dumpfile): - if dumpfile == DUMPFILE: - print "Use ``%s -R'' to restart." % sys.argv[0] - else: - print "Use ``%s -R -d %s'' to restart." % (sys.argv[0], dumpfile) + finally: + if c.save_pickle(dumpfile): + if dumpfile == DUMPFILE: + print "Use ``%s -R'' to restart." % sys.argv[0] + else: + print "Use ``%s -R -d %s'' to restart." % (sys.argv[0], + dumpfile) def load_pickle(dumpfile=DUMPFILE, verbose=VERBOSE): |