File tree 1 file changed +12
-13
lines changed
1 file changed +12
-13
lines changed Original file line number Diff line number Diff line change @@ -27,24 +27,23 @@ jobs:
27
27
lint : false
28
28
- name : Install dependencies
29
29
run : npm install
30
- - name : Install server dependencies
31
- run : |
32
- cd demo
33
- npm install
30
+ - name : Install demo
31
+ run : npm run setup_demo
34
32
- name : Build lean4monaco
35
33
run : npm run build
36
- - name : Build demo server
37
- run : |
38
- cd demo
39
- npm run build
34
+ # - name: Build demo server
35
+ # run: |
36
+ # cd demo
37
+ # npm run build
40
38
- name : Start server
41
39
id : start-server
42
40
run : |
43
- cd demo
44
- echo "Starting server..."
45
- npm run start
46
- # nohup npm run start > nohup.out 2> nohup.err < /dev/null &
47
- echo "server is running."
41
+ npm start
42
+ # cd demo
43
+ # echo "Starting server..."
44
+ # npm run start
45
+ # # nohup npm run start > nohup.out 2> nohup.err < /dev/null &
46
+ # echo "server is running."
48
47
test :
49
48
strategy :
50
49
fail-fast : false
You can’t perform that action at this time.
0 commit comments