Merge branch 'ticket31372_029' into ticket31372_035

2024-12-06 19:41:15 +01:00 · 2019-09-24 08:01:43 -04:00
parent 49a11f8a8a 6ed3d8dbd1
commit da5c8277ea
2 changed files with 8 additions and 2 deletions
@@ -0,0 +1,4 @@
+  o Minor features (continuous integration):
+    - When building on Travis, pass the "-k" flag to make, so that
+      we are informed of all compilation failures, not just the first
+      one or two. Closes part of ticket 31372.