diff options
| author | Théo Zimmermann | 2019-02-16 16:03:11 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert | 2019-02-18 21:24:11 +0100 |
| commit | b16cea4007e4286d596a46bce80815939bca271d (patch) | |
| tree | 3c4eab3e78c364e21fa88a6d610d14846547518c /dev/base_include | |
| parent | ea8a9125a4e81e7c848cf53f1e34f534d359e832 (diff) | |
Using options abort and restart of coqtop directive in the manual.
Diffstat (limited to 'dev/base_include')
0 files changed, 0 insertions, 0 deletions