From 6640d690ebdafa3ee2c38d48b791458ffda10984 Mon Sep 17 00:00:00 2001
From: Arnaud Giersch <arnaud.giersch@iut-bm.univ-fcomte.fr>
Date: Mon, 18 Jul 2011 17:39:46 +0200
Subject: [PATCH] Quick hack in run-all: compress output files.

---
 Experimentations/run-all | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/Experimentations/run-all b/Experimentations/run-all
index 638c0a5..6d556ec 100755
--- a/Experimentations/run-all
+++ b/Experimentations/run-all
@@ -120,6 +120,8 @@ for plat in "${PLATFORMS[@]}"; do
                     else
                         grep -v '/INFO\]' "$out"
                     fi
+### FIXME : make this step optional
+gzip --best "$out"
                 fi
             done
         done
-- 
2.39.5