aboutsummaryrefslogtreecommitdiff
path: root/dev/ci/user-overlays/12523-term-notation-custom.sh
AgeCommit message (Expand)Author
2020-07-03Fix #11121: Simultaneous definition of term and notation in custom grammarMaxime Dénès