On Thu, 6 Mar 2025 18:23:24 GMT, Magnus Ihse Bursie <i...@openjdk.org> wrote:
>> I don't mind removing it, my concern would be to _remember_ this option was >> there! I guess it is okay to re-re-invent it later, possibly under a >> different name, when the next port gets deprecated. > > It's no that important, no. I'm not sure if previous deprecated ports were > handles exactly like this. > > And you can always do like `git log | grep -i "remove .* port"` to find the > change it was removed in, and look what it did... I think leaving a comment describing how to deprecate a port is useful. To look it up in history you have to realise there is something to look up. "They who are not reminded of the past will invent a new way to do it in the future." ------------- PR Review Comment: https://git.openjdk.org/jdk/pull/23906#discussion_r1984572816
