@@ -195,28 +195,17 @@ runs:
195
195
if : steps.build-lean.outcome == 'success' && inputs.on_update_succeeds == 'issue' && steps.check-update.outputs.do_update == 'true'
196
196
run : | # bat
197
197
: Open issue if the updated lean build was successful
198
- CHANGED_FILES="${{ steps.check-update.outputs.changed_files }}"
199
- BULLET_LIST=""
200
- for file in $CHANGED_FILES; do
201
- BULLET_LIST="$BULLET_LIST
202
- - $file"
203
- done
204
- BODY="Files changed in update:
198
+ TITLE="Updates available and have been tested to build correctly"
199
+ DESCRIPTION=""
200
+ LABEL_NAME="auto-update-lean"
201
+ LABEL_COLOR="0E8A16"
205
202
206
- $BULLET_LIST"
207
-
208
- # Check if label exists, create it if it doesn't
209
- if ! gh api repos/${{ github.repository }}/labels/auto-update-lean --silent 2>/dev/null; then
210
- echo "Creating auto-update-lean label..."
211
- gh api repos/${{ github.repository }}/labels -F name="auto-update-lean" -F color="0E8A16" -F description="Auto update for Lean dependencies"
212
- fi
213
-
214
- gh issue create --title "$TITLE" --body "$BODY" --label "auto-update-lean"
203
+ source ${{ github.action_path }}/scripts/create-issue.sh
215
204
env :
216
205
# Could be best to use the default token here
217
206
GH_TOKEN : ${{ inputs.token }}
218
207
GH_REPO : ${{ github.repository }}
219
- TITLE : Updates available and have been tested to build correctly
208
+ CHANGED_FILES : ${{ steps.check-update.outputs.changed_files }}
220
209
shell : bash
221
210
222
211
- name : Commit update if the updated lean build was successful
@@ -235,27 +224,16 @@ runs:
235
224
if : steps.build-lean.outcome == 'failure' && inputs.on_update_fails == 'issue'
236
225
run : | # bat
237
226
: Open issue if the updated lean build fails
238
- CHANGED_FILES="${{ steps.check-update.outputs.changed_files }}"
239
- BULLET_LIST=""
240
- for file in $CHANGED_FILES; do
241
- BULLET_LIST="$BULLET_LIST
242
- - $file"
243
- done
244
- BODY="Try \`lake update\` and then investigate why this update causes the lean build to fail.
245
-
246
- Files changed in update:$BULLET_LIST"
247
-
248
- # Check if label exists, create it if it doesn't
249
- if ! gh api repos/${{ github.repository }}/labels/auto-update-lean-fail --silent 2>/dev/null; then
250
- echo "Creating auto-update-lean-fail label..."
251
- gh api repos/${{ github.repository }}/labels -F name="auto-update-lean-fail" -F color="D73A4A" -F description="Auto update for Lean dependencies"
252
- fi
227
+ TITLE="Updates available but manual intervention required"
228
+ DESCRIPTION="Try \`lake update\` and then investigate why this update causes the lean build to fail."
229
+ LABEL_NAME="auto-update-lean-fail"
230
+ LABEL_COLOR="D73A4A"
253
231
254
- gh issue create --title "$TITLE" --body "$BODY" --label "auto-update-lean-fail"
232
+ source ${{ github.action_path }}/scripts/create-issue.sh
255
233
env :
256
234
GH_TOKEN : ${{ inputs.token }}
257
235
GH_REPO : ${{ github.repository }}
258
- TITLE : " Updates available but manual intervention required "
236
+ CHANGED_FILES : ${{ steps.check-update.outputs.changed_files }}
259
237
shell : bash
260
238
261
239
- name : Action fails if the updated lean build fails
0 commit comments