copy log

egraphs-good · May 24, 2024 · 0e441ab · 0e441ab
1 parent 985b182
commit 0e441ab
Show file tree

Hide file tree

Showing 2 changed files with 4 additions and 3 deletions.
diff --git a/infra/nightly.sh b/infra/nightly.sh
@@ -69,9 +69,12 @@ popd
 # Update HTML index page.
 cp "$RESOURCE_DIR"/* "$NIGHTLY_DIR/output"
 
-# Copy json directory to the artifact
+# Copy data directory to the artifact
 cp -r "$NIGHTLY_DIR/data" "$NIGHTLY_DIR/output/data"
 
+# Copy log
+cp "$NIGHTLY_DIR/log.txt" "$NIGHTLY_DIR/output"
+
 # gzip all JSON in the nightly dir
 if [ "$LOCAL" == "" ]; then
   gzip "$NIGHTLY_DIR/output/data/profile.json"

diff --git a/infra/profile.py b/infra/profile.py
@@ -135,8 +135,6 @@ def aggregate(compile_times, bench_times):
   else:
     profiles = [bril_dir]
 
-  profiles = profiles[0:1]
-
   to_run = []
   index = 0
   total = len(profiles) * len(treatments)