Remove --default-toolchain none

pitmonticone · Jul 30, 2024 · ca8e1a8 · ca8e1a8
1 parent 532731a
commit ca8e1a8
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/.github/workflows/blueprint.yml b/.github/workflows/blueprint.yml
@@ -23,7 +23,7 @@ jobs:
           fetch-depth: 0  # Fetch all history for all branches and tags
 
       - name: Install elan
-        run: curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh -s -- -y --default-toolchain none
+        run: curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh -s -- -y
 
       - name: Get cache
         run: ~/.elan/bin/lake -Kenv=dev exe cache get || true