diff --git a/tools/make.py b/tools/make.py index c50005fbc5..6ae1e4b095 100755 --- a/tools/make.py +++ b/tools/make.py @@ -291,3 +291,5 @@ if __name__ == '__main__': traceback.print_exc(file=sys.stdout) else: print "[ERROR] %s" % str(e) + + sys.exit(1)