From 848ba0e2b8ed31cc044061306bfd4f9244946cfd Mon Sep 17 00:00:00 2001 From: Malvin Gattinger Date: Thu, 2 Nov 2023 12:54:42 +0100 Subject: [PATCH] build Bml and Pdl by default in Makefile --- .github/workflows/build.yml | 4 ++-- Makefile | 6 ++++-- 2 files changed, 6 insertions(+), 4 deletions(-) diff --git a/.github/workflows/build.yml b/.github/workflows/build.yml index 81e416f..c6ed5af 100644 --- 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 index 83a9cd1..a385a51 100644 --- 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