We should use openjdk.org instead of openjdk.java.net.
This bug was triggered by the fact that git.openjdk.java.net had problem resolving properly for GitHub Actions in the build script (and the theory is that git.openjdk.org would work better), but this should be fixed nevertheless.
This bug was triggered by the fact that git.openjdk.java.net had problem resolving properly for GitHub Actions in the build script (and the theory is that git.openjdk.org would work better), but this should be fixed nevertheless.