File tree 1 file changed +6
-6
lines changed
1 file changed +6
-6
lines changed Original file line number Diff line number Diff line change 65
65
&& github.repository == 'lampepfl/dotty'
66
66
)"
67
67
steps :
68
- - name : Set JDK 16 as default
69
- run : echo "/usr/lib/jvm/java-16 -openjdk-amd64/bin" >> $GITHUB_PATH
68
+ - name : Set JDK 17 as default
69
+ run : echo "/usr/lib/jvm/java-17 -openjdk-amd64/bin" >> $GITHUB_PATH
70
70
71
71
- name : Reset existing repo
72
72
run : git -c "http.https://github.com/.extraheader=" fetch --recurse-submodules=no "https://github.com/lampepfl/dotty" && git reset --hard FETCH_HEAD || true
@@ -116,8 +116,8 @@ jobs:
116
116
)"
117
117
118
118
steps :
119
- - name : Set JDK 16 as default
120
- run : echo "/usr/lib/jvm/java-16 -openjdk-amd64/bin" >> $GITHUB_PATH
119
+ - name : Set JDK 17 as default
120
+ run : echo "/usr/lib/jvm/java-17 -openjdk-amd64/bin" >> $GITHUB_PATH
121
121
122
122
- name : Reset existing repo
123
123
run : git -c "http.https://github.com/.extraheader=" fetch --recurse-submodules=no "https://github.com/lampepfl/dotty" && git reset --hard FETCH_HEAD || true
@@ -170,8 +170,8 @@ jobs:
170
170
)"
171
171
172
172
steps :
173
- - name : Set JDK 16 as default
174
- run : echo "/usr/lib/jvm/java-16 -openjdk-amd64/bin" >> $GITHUB_PATH
173
+ - name : Set JDK 17 as default
174
+ run : echo "/usr/lib/jvm/java-17 -openjdk-amd64/bin" >> $GITHUB_PATH
175
175
176
176
- name : Reset existing repo
177
177
run : git -c "http.https://github.com/.extraheader=" fetch --recurse-submodules=no "https://github.com/lampepfl/dotty" && git reset --hard FETCH_HEAD || true
You can’t perform that action at this time.
0 commit comments