diff options
| author | Pierre-Marie Pédrot | 2018-09-06 13:52:42 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2018-09-06 13:52:42 +0200 |
| commit | 51c5c25c944cc78b61392afdd2a19ae8f9e61614 (patch) | |
| tree | e441e02263200f38a758234a0017ebe6f208d0f5 /dune-project | |
| parent | 5b2b73762faec4f16b7b3494544f4b5788b1b73a (diff) | |
| parent | fa239fdca9fc07e65aec424c9a0c88128c43c329 (diff) | |
Merge PR #8394: Print the entire string to the CoqIDE screen, e.g. for "Print Options"
Diffstat (limited to 'dune-project')
0 files changed, 0 insertions, 0 deletions