File tree Expand file tree Collapse file tree
Expand file tree Collapse file tree Original file line number Diff line number Diff line change 55 tags :
66 - ' *'
77 workflow_dispatch :
8+ inputs :
9+ disable_docker_cache :
10+ type : boolean
11+ description : Forces docker image rebuild
12+ default : false
13+ skip_release :
14+ type : boolean
15+ description : Do not create a release from this run
16+ default : false
817
918jobs :
1019 build-latex :
1726 - name : Checkout
1827 uses : actions/checkout@v4
1928
29+ - name : Cache Docker Image
30+ uses : ScribeMD/docker-cache@0.5.0
31+ if : ${{ ! github.event.inputs.disable_docker_cache }}
32+ with :
33+ key : docker-${{ runner.os }}-${{ hashFiles('.devcontainer/Dockerfile') }}
34+
2035 - name : Build image
2136 run : |
2237 docker build \
3449
3550 - name : Create Release
3651 uses : softprops/action-gh-release@v2
52+ if : ${{ ! github.event.inputs.skip_release }}
3753 with :
3854 name : Release ${{ github.ref_name }}
3955 generate_release_notes : true
You can’t perform that action at this time.
0 commit comments