Merge branch 'master' into master

1 files changed, 15 insertions, 0 deletions

diff --git a/tools/print_status.py b/tools/print_status.py
new file mode 100755
index 000000000..ed563fd68
--- /dev/null
+++ b/tools/print_status.py
@@ -0,0 +1,15 @@
+#!/usr/bin/env python3
+
+import sys
+if len(sys.argv) != 2:
+    print("""\
+Usage: print_status.py STATUS_FILENAME
+    STATUS_FILENAME contains one line with an integer status."""
+    )
+    sys.exit(1)
+with open(sys.argv[1], 'r') as status_in:
+    status = int(status_in.readline())
+
+print('{} with status {}'.format(
+    "\033[32msucceeded\033[0m" if status == 0 else "\033[31mfailed\033[0m",
+    status))