From 6de68dd8efb308e10f7e6ed112af76331b11216c Mon Sep 17 00:00:00 2001
From: Cameron Zwarich <cameron@lean-fro.org>
Date: Mon, 7 Jul 2025 22:49:57 -0700
Subject: [PATCH] chore: remove compiler.enableNew=true from a test and rename
 it (#9247)

---
 tests/lean/run/{opaqueNewCodeGen.lean => opaqueCodeGen.lean} | 4 +---
 1 file changed, 1 insertion(+), 3 deletions(-)
 rename tests/lean/run/{opaqueNewCodeGen.lean => opaqueCodeGen.lean} (77%)

diff --git a/tests/lean/run/opaqueNewCodeGen.lean b/tests/lean/run/opaqueCodeGen.lean
similarity index 77%
rename from tests/lean/run/opaqueNewCodeGen.lean
rename to tests/lean/run/opaqueCodeGen.lean
index fd46a297bb..bff9a111f9 100644
--- a/tests/lean/run/opaqueNewCodeGen.lean
+++ b/tests/lean/run/opaqueCodeGen.lean
@@ -1,7 +1,5 @@
 import Lean
 
-set_option compiler.enableNew true
-
 /--
 trace: [Compiler.result] size: 1
     def f x : Nat :=
@@ -15,7 +13,7 @@ opaque f : Nat → Nat :=
 
 /--
 trace: [Compiler.result] size: 0
-    def g a._@.opaqueNewCodeGen._hyg.1 a._@.opaqueNewCodeGen._hyg.2 : Nat :=
+    def g a._@.opaqueCodeGen._hyg.1 a._@.opaqueCodeGen._hyg.2 : Nat :=
       extern
 -/
 #guard_msgs in