build Bml and Pdl by default in Makefile

m4lvin · Nov 2, 2023 · 848ba0e · 848ba0e
1 parent 3cd19ae
commit 848ba0e
Show file tree

Hide file tree

Showing 2 changed files with 6 additions and 4 deletions.
diff --git a/.github/workflows/build.yml b/.github/workflows/build.yml
@@ -22,8 +22,8 @@ jobs:
           ~/.elan/bin/lean --version
           echo "$HOME/.elan/bin" >> $GITHUB_PATH
 
-      - name: make
-        run: make
+      - name: make pdl
+        run: make pdl
 
   bml:
     name: Build Bml

diff --git a/Makefile b/Makefile
@@ -1,6 +1,8 @@
 
-default: .first-run-done
-	lake build
+all: pdl bml
+
+pdl: .first-run-done
+	lake build Pdl
 
 bml: .first-run-done
 	lake build Bml