diff options
| author | Théo Zimmermann | 2019-02-16 16:42:52 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert | 2019-02-19 13:07:13 +0100 |
| commit | 499491f8efd3a02dacb64c779edc246510b1d35f (patch) | |
| tree | 04acdbeade11b3207d743c24ff039bda33d2caae /doc/plugin_tutorial/tuto1/src | |
| parent | b16cea4007e4286d596a46bce80815939bca271d (diff) | |
[sphinx] Refactor handling of options for coqtop directive.
Make it mandatory to give exactly one display option.
Diffstat (limited to 'doc/plugin_tutorial/tuto1/src')
0 files changed, 0 insertions, 0 deletions