This resolves #808 (closed).
Pipeline #118000 passed
Pipeline passed for 0dd8beba on j.gui15 1 year ago
Merge details
Closed #808 (closed)
Pipeline #118002 passed
Pipeline passed for 823b13ea on main 1 year ago
added 1 commit
Compare with previous version
merged
mentioned in commit 823b13ea