Merge pull request 'dev' (#17) from dev into main
Reviewed-on: #17
This commit was merged in pull request #17.
This commit is contained in:
@@ -11,6 +11,7 @@ jobs:
|
||||
build-image:
|
||||
name: Build Docker image
|
||||
runs-on: ubuntu-latest
|
||||
if: ${{ !contains(github.event.pull_request.title, '[skip-ci]') }}
|
||||
|
||||
steps:
|
||||
- name: Checkout repository
|
||||
|
||||
Reference in New Issue
Block a user