Skip to content

introduce [default] as abbreviation for [from_option id], and use it

Ralf Jung requested to merge ralf/default into master

There's some more uses in Iris, so this seems worth it. Over std++ and Iris together, the new default will actually be used more often than the old one I removed in !31 (merged).

Merge request reports