aboutsummaryrefslogtreecommitdiff
path: root/plugins/syntax/plugin_base.dune
diff options
context:
space:
mode:
authorMatthieu Sozeau2018-09-20 17:12:12 +0200
committerMatthieu Sozeau2018-09-20 17:12:12 +0200
commit7b6f1f0ed0872cd16d7d01683673fd9323122f30 (patch)
tree2d3e6141d9dd38cc483df6a5ce6a59854519f047 /plugins/syntax/plugin_base.dune
parentdf1f5bcd406a87c77601942f21d16555a8f6086e (diff)
parent69339f8fcfe3e5f3fa1c58feba6b0740c7e86538 (diff)
Merge PR #8297: Fix #7754: universe declarations on mutual inductives
Diffstat (limited to 'plugins/syntax/plugin_base.dune')
0 files changed, 0 insertions, 0 deletions