diff --git a/.github/workflows/ci.yaml b/.github/workflows/ci.yaml index 1f60ab5b0236..caea27d8f682 100644 --- a/.github/workflows/ci.yaml +++ b/.github/workflows/ci.yaml @@ -46,8 +46,8 @@ jobs: && github.repository == 'lampepfl/dotty' )" steps: - - name: Set JDK 16 as default - run: echo "/usr/lib/jvm/java-16-openjdk-amd64/bin" >> $GITHUB_PATH + - name: Set JDK 17 as default + run: echo "/usr/lib/jvm/java-17-openjdk-amd64/bin" >> $GITHUB_PATH - name: Reset existing repo run: git -c "http.https://github.com/.extraheader=" fetch --recurse-submodules=no "https://github.com/lampepfl/dotty" && git reset --hard FETCH_HEAD || true @@ -91,8 +91,8 @@ jobs: )" steps: - - name: Set JDK 16 as default - run: echo "/usr/lib/jvm/java-16-openjdk-amd64/bin" >> $GITHUB_PATH + - name: Set JDK 17 as default + run: echo "/usr/lib/jvm/java-17-openjdk-amd64/bin" >> $GITHUB_PATH - name: Reset existing repo run: git -c "http.https://github.com/.extraheader=" fetch --recurse-submodules=no "https://github.com/lampepfl/dotty" && git reset --hard FETCH_HEAD || true