X-Git-Url: https://pintos-os.org/cgi-bin/gitweb.cgi?p=pspp;a=blobdiff_plain;f=build-pspp;h=16c19cf0e8c781910c9724fcf83b164fee6c9903;hp=09a0e89c375c71eefb743c175253b259ba60b39b;hb=HEAD;hpb=8a0733b930a5f1c13321b08981b06262edad78ce

diff --git a/build-pspp b/build-pspp
index 09a0e89c37..b449a5c89c 100755
--- a/build-pspp
+++ b/build-pspp
@@ -117,6 +117,7 @@ def write_timing(id, time):
 
 
 def fail():
+    set_var("result", "failure")
     sys.stderr.write("Build failed, refer to:\n\t%s\nfor details.\n" % logfile)
     sys.exit(1)
 
@@ -414,7 +415,7 @@ if len(args) == 2:
     if gnulib_commit is None:
         sys.stderr.write("%s does not specify a Git commit number\n"
                          % fullname)
-        sys.exit(1)
+        fail()
     set_var("gnulib_commit", gnulib_commit)
 
     version = add_commit_to_version("pspp", revision, "pspp",
@@ -586,3 +587,4 @@ if build_binary:
     # distcleancheck
 
 start_step("Success")
+set_var("result", "success")