Subject: [patch] Add Java 17
From: Ricardo Wurmus <[email-masked]>
To: [email-masked]
Cc: "Dr. Arne Babenhauserheide" <[email-masked]>
Date: Thu, 02 Dec 2021 22:58:29 +0000
List-Id: <debbugs-submit.debbugs.gnu.org>

I split it up into a commit fixing openjdk 16 and one adding openjdk 17;
I removed a duplicate phase from openjdk 17 and let it inherit the phases from openjdk 16.

I’ve applied the patches to the “master” branch.

Thanks!

-- 
Ricardo