Closed stephengold closed 11 months ago
GitHub claims this PR was merged into "master" branch at commit 149817a (3 December 2023). However, the javadoc in the "master" branch still indicates the incorrect default:
Also, I can't find commit 149817a in my clone of the repo:
$ git checkout -b qqq 149817a
fatal: '149817a' is not a commit and a branch 'qqq' cannot be created from it
$
I don't know how this happened. Perhaps that commit was destroyed by a force push?
I plan to re-open issue #2142 and submit a new PR.
Ready for review.