Also remove Duper from annotation [annotate]

utensil · Oct 22, 2024 · 28f17e0 · 28f17e0
1 parent 3197033
commit 28f17e0
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/lean4/scripts/annotate.lean b/lean4/scripts/annotate.lean
@@ -21,7 +21,7 @@ def main (args : List String) : IO Unit := do
 
   _ ← (← IO.Process.spawn { cmd := "lake", args := #["build"] }).wait
   -- Duper requires some additional time to build on first run.
-  _ ← (← IO.Process.spawn { cmd := "lake", args := #["build", "Duper"] }).wait
+  -- _ ← (← IO.Process.spawn { cmd := "lake", args := #["build", "Duper"] }).wait
 
   -- Collect test targets by walking `Playground/` and `Playground/Zulip`.
   -- let noNoisy := args.contains "--no-noisy"