run-all: report error messages on failure.

diff --git a/Experimentations/run-all b/Experimentations/run-all
index 5584528a48d3f5cef2a4d6438e57f3a2977b324a..638c0a5997ba9f7d7d530087351fc4477a011c0b 100755 (executable)
--- a/Experimentations/run-all
+++ b/Experimentations/run-all
@@ -115,8 +115,11 @@ for plat in "${PLATFORMS[@]}"; do
                     log "skipped (dry-run)"
                 else
                     echo "# ${cmd[@]}" > "$out"
                     log "skipped (dry-run)"
                 else
                     echo "# ${cmd[@]}" > "$out"

-                    "${cmd[@]}" >> "$out" 2>&1
-                    summary "$out"
+                    if "${cmd[@]}" >> "$out" 2>&1; then
+                        summary "$out"
+                    else
+                        grep -v '/INFO\]' "$out"
+                    fi

                 fi
             done
         done
                 fi
             done
         done