aboutsummaryrefslogtreecommitdiffhomepage
path: root/dev/ci/gitlab.bat
diff options
context:
space:
mode:
authorGravatar Emilio Jesus Gallego Arias <e+git@x80.org>2018-05-24 03:15:17 +0200
committerGravatar Emilio Jesus Gallego Arias <e+git@x80.org>2018-05-31 11:16:47 +0200
commit63b530234e0b19323a50c52434a7439518565c81 (patch)
tree12c19a5ffbbb08fade444b7ec495e44090dfad14 /dev/ci/gitlab.bat
parent2a69be9e8243fa67d5c7ef5f10e623b02a0a3e2f (diff)
[notations] Split interpretation and parsing of notations
Previously to this patch, `Notation_term` contained information about both parsing and notation interpretation. We split notation grammar to a file `parsing/notation_gram` as to make `interp/` not to depend on some parsing structures such as entries.
Diffstat (limited to 'dev/ci/gitlab.bat')
0 files changed, 0 insertions, 0 deletions