mirror of
https://github.com/maxkratz/edgedb.git
synced 2024-09-16 18:59:05 +00:00
GH job to check that postgres/ has not been unintentianally changed, take 2 (#6715)
This commit is contained in:
parent
a8e2933dc2
commit
18c7f69445
1 changed files with 9 additions and 7 deletions
|
@ -1,7 +1,7 @@
|
|||
name: Pull Request
|
||||
name: Pull Request Meta
|
||||
|
||||
on:
|
||||
pull_request_target:
|
||||
pull_request:
|
||||
types: [opened, edited, synchronize, labeled, closed]
|
||||
|
||||
concurrency:
|
||||
|
@ -28,12 +28,14 @@ jobs:
|
|||
exit 0
|
||||
fi
|
||||
|
||||
git diff --quiet \
|
||||
if git diff --quiet \
|
||||
${{ github.event.pull_request.base.sha }} \
|
||||
${{ github.event.pull_request.head.sha }}
|
||||
if [ $? != 0 ]; then
|
||||
${{ github.event.pull_request.head.sha }} -- postgres/
|
||||
then
|
||||
echo 'all ok'
|
||||
else
|
||||
echo "postgres/ submodule has been changed,"\
|
||||
"but PR title does not indicate that" 1>&2
|
||||
echo "(it should start with '$required_prefix')" 1>&2
|
||||
"but PR title does not indicate that"
|
||||
echo "(it should start with '$required_prefix')"
|
||||
exit 1
|
||||
fi
|
Loading…
Reference in a new issue