File tree Expand file tree Collapse file tree 2 files changed +4
-10
lines changed Expand file tree Collapse file tree 2 files changed +4
-10
lines changed Original file line number Diff line number Diff line change @@ -1528,11 +1528,6 @@ jobs:
15281528 uses : taiki-e/install-action@v2
15291529 with :
15301530 tool : mdbook
1531- - name : Prepare directories
1532- run : |
1533- mkdir -p ${{ runner.temp }}/book
1534- mkdir -p ${{ runner.temp }}/book/devel
1535- mkdir -p ${{ runner.temp }}/book/dev-guide
15361531 - name : Build user-guide (stable)
15371532 if : ${{ !contains('["pull_request", "merge_group"]', github.event_name) }}
15381533 run : |
@@ -1546,12 +1541,14 @@ jobs:
15461541 git checkout master
15471542 cd doc/user-guide
15481543 mdbook build
1544+ mkdir -p ${{ runner.temp }}/book
15491545 mv book ${{ runner.temp }}/book/devel
15501546 - name : Build dev-guide (master)
15511547 run : |
15521548 git checkout master
15531549 cd doc/dev-guide
15541550 mdbook build
1551+ mkdir -p ${{ runner.temp }}/book
15551552 mv book ${{ runner.temp }}/book/dev-guide
15561553 - name : Deploy to GitHub
15571554 if : ${{ !contains('["pull_request", "merge_group"]', github.event_name) }}
Original file line number Diff line number Diff line change @@ -15,11 +15,6 @@ jobs: # skip-all
1515 uses : taiki-e/install-action@v2
1616 with :
1717 tool : mdbook
18- - name : Prepare directories
19- run : |
20- mkdir -p ${{ runner.temp }}/book
21- mkdir -p ${{ runner.temp }}/book/devel
22- mkdir -p ${{ runner.temp }}/book/dev-guide
2318 - name : Build user-guide (stable)
2419 if : ${{ !contains('["pull_request", "merge_group"]', github.event_name) }}
2520 run : |
@@ -33,12 +28,14 @@ jobs: # skip-all
3328 git checkout master
3429 cd doc/user-guide
3530 mdbook build
31+ mkdir -p ${{ runner.temp }}/book
3632 mv book ${{ runner.temp }}/book/devel
3733 - name : Build dev-guide (master)
3834 run : |
3935 git checkout master
4036 cd doc/dev-guide
4137 mdbook build
38+ mkdir -p ${{ runner.temp }}/book
4239 mv book ${{ runner.temp }}/book/dev-guide
4340 - name : Deploy to GitHub
4441 if : ${{ !contains('["pull_request", "merge_group"]', github.event_name) }}
You can’t perform that action at this time.
0 commit comments