resolve merge conflict

leanprover · Nov 16, 2023 · dde2ea9 · dde2ea9
2 parents a65c377 + 19207d2
commit dde2ea9
Show file tree

Hide file tree

Showing 2 changed files with 6 additions and 1 deletion.
diff --git a/.github/workflows/test.yml b/.github/workflows/test.yml
@@ -6,6 +6,7 @@ name: continuous integration
 jobs:
   build:
     name: test
+    runs-on: ubuntu-latest
     steps:
       - name: install elan
         run: |

diff --git a/test.sh b/test.sh
@@ -34,7 +34,11 @@ check_command "lake exe lean4checker Lean4CheckerTests.AddFalseConstructor" "unc
 
 check_command "lake exe lean4checker --fresh Lean4CheckerTests.UseFalseConstructor" "uncaught exception: (kernel) unknown constant 'False.intro'"
 
-check_command "lake exe lean4checker Lean4CheckerTests.ReduceBool" "uncaught exception: (kernel) unknown declaration 'foo'"
+# The 'ReduceBool' test writes to a temporary file.
+# We clean up before and afterwards for consistency, although neither should be required.
+rm -f .lean4checker.tmp
+check_command "lake exe lean4checker Lean4Checker.Tests.ReduceBool" "uncaught exception: (kernel) unknown declaration 'foo'"
+rm -f .lean4checker.tmp
 
 check_command "lake exe lean4checker Lean4CheckerTests.OverridenPrelude" "TODO"
-Original file line number
+Diff line change
@@ Expand Up / @@ -6,6 +6,7 @@ name: continuous integration @@
     jobs:
       build:
         name: test
+        runs-on: ubuntu-latest
         steps:
           - name: install elan
             run: |
@@ Expand Down @@