fix: don't show noisy dumps during build

leanprover · Mar 5, 2024 · 5052542 · 5052542
1 parent 4bb7a97
commit 5052542
Showing 1 changed file with 2 additions and 4 deletions.
diff --git a/src/examples/SubVerso/Examples.lean b/src/examples/SubVerso/Examples.lean
@@ -144,12 +144,10 @@ def wxyz (n : Nat) := 1 + 3 + n
 def xyz (n : Nat) := 1 + %ex{test2}{3 + n}
 %end
 
---%process_highlights
-
 -- %example test
 -- #eval 5
 -- %end
 
 -- %dump test
-%dump test3.test2
-%dump test3
+-- %dump test3.test2
+-- %dump test3