Merge pull request #52 from Peiyang-Song/main

Add CI for PR targeting main
lean-dojo · Jan 22, 2024 · 8c7b338 · 8c7b338
2 parents 78b2baa + 07e438e
commit 8c7b338
Show file tree

Hide file tree

Showing 3 changed files with 5 additions and 3 deletions.
diff --git a/.dockerignore b/.dockerignore
@@ -1,7 +1,6 @@
 *.txt
 .vscode
 tmp
-lake-packages
 .lake
 clang+llvm*
 python/__pycache__
diff --git a/.github/workflows/push.yml → .github/workflows/push_pr.yml b/.github/workflows/push.yml → .github/workflows/push_pr.yml
@@ -1,6 +1,10 @@
 name: CI
 
 on:
+  pull_request:
+    branches:
+      - main
+
   push:
     branches:
       - main

diff --git a/.gitignore b/.gitignore
@@ -1,5 +1,4 @@
-/lake-packages/*
-/.lake
+.lake
 
 .vscode
 *.olean
-Original file line number
+Diff line change
@@ -1,5 +1,4 @@
-    /lake-packages/*
-    /.lake
+    .lake
     .vscode
     *.olean
@@ Expand Down @@