devops: Tolerate make check failures.

diff --git a/src/devops/devops.scm b/src/devops/devops.scm
index b6b25ae7df10d46f74fa65aaf63de8dcd232c49c..154996276f21094291e1274cdb1cd6b5f12d2c04 100644 (file)
--- a/src/devops/devops.scm
+++ b/src/devops/devops.scm
@@ -855,7 +855,7 @@ Inc., 51 Franklin St, Fifth Floor, Boston, MA 02110-1301, USA.
     (trun "cd src/ && make tags")
     (trun "cd src/ && make all")
     (lndir "../tests")
-    (trun "cd src/ && make check")
+    (trun-noerror "cd src/ && make check")
     (trun "cd src/ && umask 022 && make install")
 
     (let ((plugin-errors
@@ -991,6 +991,13 @@ Inc., 51 Franklin St, Fifth Floor, Boston, MA 02110-1301, USA.
   (log "# "(emacs-friendly-timestamp)"\n")
   (apply run strings))
 
+(define (trun-noerror . strings)
+  (log "# "(emacs-friendly-timestamp)"\n")
+  (let* ((cmdln (string* strings))
+        (status (run-noerror cmdln)))
+    (if (not (zero? status))
+       (warn "Shell command failed:" status cmdln))))
+
 (define (emacs-friendly-timestamp)
   (let ((dt (local-decoded-time)))
     (define (pad num) (string-pad-left (number->string num) 2 #\0))