"Generalise" lake update (#36)

oliver-butterley · Sep 25, 2024 · de5132e · de5132e
1 parent d744c3d
commit de5132e
Showing 1 changed file with 2 additions and 2 deletions.
diff --git a/action.yml b/action.yml
@@ -41,7 +41,7 @@ runs:
       shell: bash
 
     - name: Update dependencies of ${{ github.repository }}
-      run: lake update
+      run: lake -R -Kenv=dev update
       shell: bash
 
     - name: Check if lean-toolchain or lake-manifest.json were updated
@@ -77,7 +77,7 @@ runs:
       if: steps.build-lean.outcome == 'success' && inputs.on_update_succeeds == 'pr'
       uses: peter-evans/create-pull-request@v7
       with:
-        title: "Updates available and ready to merge."
+        title: "Updates available and ready to merge"
         body: "To do: add useful details here..."
         delete-branch: true
         branch-suffix: random