Index: gcl.py |
diff --git a/gcl.py b/gcl.py |
index a32b950fe48f9ad4ea88ed00b9f3cee46d6a5c69..cf657893c737133e5266ad8ff27bb052295f2ee0 100755 |
--- a/gcl.py |
+++ b/gcl.py |
@@ -1511,4 +1511,8 @@ def main(argv): |
if __name__ == "__main__": |
fix_encoding.fix_encoding() |
- sys.exit(main(sys.argv[1:])) |
+ try: |
+ sys.exit(main(sys.argv[1:])) |
+ except KeyboardInterrupt: |
+ sys.stderr.write('interrupted\n') |
+ sys.exit(1) |