File tree 5 files changed +28
-15
lines changed
5 files changed +28
-15
lines changed Original file line number Diff line number Diff line change
1
+ name : CI
2
+
3
+ on :
4
+ push :
5
+ branches :
6
+ - ' master'
7
+ tags : ' *'
8
+ pull_request :
9
+
10
+ jobs :
11
+ build :
12
+ name : Page build
13
+ runs-on : ubuntu-latest
14
+ steps :
15
+ - uses : actions/checkout@v2
16
+ - uses : julia-actions/setup-julia@v1
17
+ with :
18
+ version : ' 1'
19
+ - name : Install dependencies
20
+ run : julia --project -e 'using Pkg; Pkg.instantiate()'
21
+ - name : Build and deploy
22
+ env :
23
+ GITHUB_TOKEN : ${{ secrets.GITHUB_TOKEN }}
24
+ DOCUMENTER_KEY : ${{ secrets.DOCUMENTER_KEY }}
25
+ run : julia --project --color=yes make.jl
Load Diff This file was deleted.
Original file line number Diff line number Diff line change @@ -3,4 +3,4 @@ Documenter = "e30172f5-a6a5-5a46-863b-614d45cd2de4"
3
3
Markdown = " d6f4376e-aef5-505a-96c1-9c027394607a"
4
4
5
5
[compat ]
6
- Documenter = " 0.22 "
6
+ Documenter = " 0.27.3 "
Original file line number Diff line number Diff line change @@ -56,4 +56,6 @@ deploydocs(
56
56
repo = " github.com/JuliaDocs/juliadocs.github.io.git" ,
57
57
branch = " master" ,
58
58
devbranch = " source" ,
59
+ versions = nothing ,
60
+ push_preview = true ,
59
61
)
You can’t perform that action at this time.
0 commit comments