Quick hack in run-all: compress output files.

diff --git a/Experimentations/run-all b/Experimentations/run-all
index 638c0a5997ba9f7d7d530087351fc4477a011c0b..6d556ec532a409ba6513d1a624ace8b40b1bcc37 100755 (executable)
--- a/Experimentations/run-all
+++ b/Experimentations/run-all
@@ -120,6 +120,8 @@ for plat in "${PLATFORMS[@]}"; do
                     else
                         grep -v '/INFO\]' "$out"
                     fi
                     else
                         grep -v '/INFO\]' "$out"
                     fi

+### FIXME : make this step optional
+gzip --best "$out"

                 fi
             done
         done
                 fi
             done
         done