handle file exists, update log path

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

Hide file tree

Showing 2 changed files with 5 additions and 2 deletions.
diff --git a/infra/nightly-resources/index.html b/infra/nightly-resources/index.html
@@ -79,7 +79,7 @@ <h2>Raw</h2>
     <a href="table.html?table=benchmarks">Nightly Table</a>
   </p>
   <p>
-    <a href="data/log.txt">Log</a>
+    <a href="log.txt">Log</a>
   </p>
 </body>
 

diff --git a/infra/profile.py b/infra/profile.py
@@ -124,7 +124,10 @@ def aggregate(compile_times, bench_times):
     exit(1)
 
   # Create tmp directory for intermediate files
-  os.mkdir(TMP_DIR)
+  try:
+    os.mkdir(TMP_DIR)
+  except FileExistsError:
+    print(f"{TMP_DIR} exits, overwriting contents")
 
   bril_dir, DATA_DIR = os.sys.argv[1:]
   profiles = []