aboutsummaryrefslogtreecommitdiff
path: root/dev/ci/user-overlays/12523-term-notation-custom.sh
AgeCommit message (Collapse)Author
2020-10-12Automatically merge overlays with most recent upstream versionGaëtan Gilbert
This avoids the need to rebase the overlay when nothing has changed.
2020-07-03Fix #11121: Simultaneous definition of term and notation in custom grammarMaxime Dénès