File tree 2 files changed +4
-10
lines changed
2 files changed +4
-10
lines changed Original file line number Diff line number Diff line change @@ -1528,11 +1528,6 @@ jobs:
1528
1528
uses : taiki-e/install-action@v2
1529
1529
with :
1530
1530
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
1536
1531
- name : Build user-guide (stable)
1537
1532
if : ${{ !contains('["pull_request", "merge_group"]', github.event_name) }}
1538
1533
run : |
@@ -1546,12 +1541,14 @@ jobs:
1546
1541
git checkout master
1547
1542
cd doc/user-guide
1548
1543
mdbook build
1544
+ mkdir -p ${{ runner.temp }}/book
1549
1545
mv book ${{ runner.temp }}/book/devel
1550
1546
- name : Build dev-guide (master)
1551
1547
run : |
1552
1548
git checkout master
1553
1549
cd doc/dev-guide
1554
1550
mdbook build
1551
+ mkdir -p ${{ runner.temp }}/book
1555
1552
mv book ${{ runner.temp }}/book/dev-guide
1556
1553
- name : Deploy to GitHub
1557
1554
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
15
15
uses : taiki-e/install-action@v2
16
16
with :
17
17
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
23
18
- name : Build user-guide (stable)
24
19
if : ${{ !contains('["pull_request", "merge_group"]', github.event_name) }}
25
20
run : |
@@ -33,12 +28,14 @@ jobs: # skip-all
33
28
git checkout master
34
29
cd doc/user-guide
35
30
mdbook build
31
+ mkdir -p ${{ runner.temp }}/book
36
32
mv book ${{ runner.temp }}/book/devel
37
33
- name : Build dev-guide (master)
38
34
run : |
39
35
git checkout master
40
36
cd doc/dev-guide
41
37
mdbook build
38
+ mkdir -p ${{ runner.temp }}/book
42
39
mv book ${{ runner.temp }}/book/dev-guide
43
40
- name : Deploy to GitHub
44
41
if : ${{ !contains('["pull_request", "merge_group"]', github.event_name) }}
You can’t perform that action at this time.
0 commit comments