diff options
| author | Guillaume Melquiond | 2021-01-13 18:29:11 +0100 |
|---|---|---|
| committer | Guillaume Melquiond | 2021-01-13 21:03:41 +0100 |
| commit | e881720a724ffa4e6201cc1d460c66ce373713d9 (patch) | |
| tree | e9e70f031996d23609f5d8ef5fd1b381646189fd /plugins/syntax | |
| parent | 9fef12aadf0e7afea3d89a00cb7216b2b008cf5c (diff) | |
Make sure "Print Module" write a dot at the end of inductive definitions.
Diffstat (limited to 'plugins/syntax')
0 files changed, 0 insertions, 0 deletions