File tree 1 file changed +7
-7
lines changed
1 file changed +7
-7
lines changed Original file line number Diff line number Diff line change @@ -154,13 +154,13 @@ jobs:
154
154
cabal run GenerateEverything
155
155
cp travis/* .
156
156
./index.sh
157
- # ${{ env.AGDA }} --safe EverythingSafe.agda
158
- # ${{ env.AGDA }} index.agda
157
+ ${{ env.AGDA }} --safe EverythingSafe.agda
158
+ ${{ env.AGDA }} index.agda
159
159
160
- # - name: Golden testing
161
- # run: |
162
- # ${{ env.CABAL_INSTALL }} clock
163
- # make testsuite INTERACTIVE='' AGDA_EXEC='~/.cabal/bin/agda'
160
+ - name : Golden testing
161
+ run : |
162
+ ${{ env.CABAL_INSTALL }} clock
163
+ make testsuite INTERACTIVE='' AGDA_EXEC='~/.cabal/bin/agda'
164
164
165
165
166
166
# #######################################################################
@@ -183,7 +183,7 @@ jobs:
183
183
184
184
- name : Deploy HTML
185
185
186
- # if: ${{ success() && env.AGDA_DEPLOY }}
186
+ if : ${{ success() && env.AGDA_DEPLOY }}
187
187
188
188
with :
189
189
branch : gh-pages
You can’t perform that action at this time.
0 commit comments