On Thu, 19 Jan 2023 12:35:37 GMT, Jiří Vaněk <jvanek at openjdk.org> wrote: > Reviewed-by: mgronlun Actually, the lib should be @library /lib / ? ------------- PR: https://git.openjdk.org/jdk8u-dev/pull/234