File tree 1 file changed +17
-7
lines changed
1 file changed +17
-7
lines changed Original file line number Diff line number Diff line change @@ -32,17 +32,27 @@ jobs:
32
32
build : true
33
33
test : false
34
34
lint : false
35
- - name : install elan (Windows)
36
- if : matrix.os == 'windows-latest'
37
- run : |
38
- curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf > elan-init.sh
39
- sh elan-init.sh -y
40
- echo "$HOME/.elan/bin" >> $GITHUB_PATH
41
- - name : lean bui.d (Windows)
35
+ - name : install elan
42
36
if : matrix.os == 'windows-latest'
43
37
run : |
38
+ curl -O --location https://raw.githubusercontent.com/leanprover/elan/master/elan-init.ps1
39
+ echo 1 | powershell -ExecutionPolicy Bypass -f elan-init.ps1
40
+ del elan-init.ps1
41
+ (Resolve-Path ~/.elan/bin).Path >> $Env:GITHUB_PATH
44
42
cd demo\server\LeanProject
45
43
lake build
44
+ shell : pwsh
45
+ # - name: install elan (Windows)
46
+ # if: matrix.os == 'windows-latest'
47
+ # run: |
48
+ # curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf > elan-init.sh
49
+ # sh elan-init.sh -y
50
+ # echo "$HOME/.elan/bin" >> $GITHUB_PATH
51
+ # - name: lean bui.d (Windows)
52
+ # if: matrix.os == 'windows-latest'
53
+ # run: |
54
+ # cd demo\server\LeanProject
55
+ # lake build
46
56
- uses : actions/setup-node@v3
47
57
- run : npm install --loglevel verbose
48
58
- run : npm audit
You can’t perform that action at this time.
0 commit comments