Closed thomas-fossati closed 2 years ago
Partly addressing #170
Should this PR also remove #6.500 global tag?
I don't think we reached full consensus on that point: in particular, Henk was not sure. See third bullet point in #170.
Partly addressing #170