diff options
| author |  Théo Zimmermann <theo.zimmermann@univ-paris-diderot.fr> | 2018-07-02 19:04:18 +0200 |
|---|---|---|
| committer | Théo Zimmermann <theo.zimmermann@univ-paris-diderot.fr> | 2018-07-02 19:04:18 +0200 |
| commit | 0a556686f5c759e61dc740dd1b2762a077a19f40 (patch) | |
| tree | 68cb03e948f69babc5a9ca2e76b73cb46d8c3d66 /doc/sphinx/user-extensions/syntax-extensions.rst | |
| parent | 02fe76c0c1c3f01c6fb4310dd4450b35f43005da (diff) | |
| parent | 905770ed2a8b9b760b9a8c1384d4d65cdb82892e (diff) | |
Merge PR #7965: doc: Fix typesetting in Gallina extensions
Diffstat (limited to 'doc/sphinx/user-extensions/syntax-extensions.rst')
0 files changed, 0 insertions, 0 deletions