aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping
diff options
context:
space:
mode:
authorGravatar Matthieu Sozeau <matthieu.sozeau@inria.fr>2018-06-05 12:08:08 +0200
committerGravatar Matthieu Sozeau <matthieu.sozeau@inria.fr>2018-06-05 12:08:08 +0200
commitaf65c79cc976f3f96a768f3d0897febb24e1485a (patch)
tree13a928e685c5def05ce57eb3227eca75286bc8ba /pretyping
parent56be411d5c582d6f644129dabda7ba036a4419a7 (diff)
parent160e9f8c7d1af2357db4a37d834b0b9bb28632fb (diff)
Merge PR #7453: Refuse to parse empty [Context] command.
Diffstat (limited to 'pretyping')
0 files changed, 0 insertions, 0 deletions