aboutsummaryrefslogtreecommitdiff
path: root/doc/plugin_tutorial/tuto2
diff options
context:
space:
mode:
authorGuillaume Melquiond2021-01-13 18:29:11 +0100
committerGuillaume Melquiond2021-01-13 21:03:41 +0100
commite881720a724ffa4e6201cc1d460c66ce373713d9 (patch)
treee9e70f031996d23609f5d8ef5fd1b381646189fd /doc/plugin_tutorial/tuto2
parent9fef12aadf0e7afea3d89a00cb7216b2b008cf5c (diff)
Make sure "Print Module" write a dot at the end of inductive definitions.
Diffstat (limited to 'doc/plugin_tutorial/tuto2')
0 files changed, 0 insertions, 0 deletions