Add a VERSION file, for the distrib.

[loba.git] / Experimentations / run-all

diff --git a/Experimentations/run-all b/Experimentations/run-all
index c7115502b587bb86980f19d71e154a419ece9ef9..5b80fbf49f0f40f2491b4bf81aa2f5ab5a327195 100755 (executable)
--- a/Experimentations/run-all
+++ b/Experimentations/run-all
@@ -74,7 +74,10 @@ COMMON_OPTS=(
     "${MORE_ARGS[@]}"
 )
 
     "${MORE_ARGS[@]}"
 )
 

-test -x "$LOBA" || die "command not found: \"$LOBA\""
+test -f "$LOBA" && test -x "$LOBA" || die "command not found: \"$LOBA\""
+for plat in "${PLATFORMS[@]}"; do
+    test -f "$plat" && test -r "$plat" || die "file not found: \"$plat\""
+done

 
 log "Results put in: \"$RESULTS\"."
 
 
 log "Results put in: \"$RESULTS\"."