diff options
| author | Hugo Herbelin | 2020-02-23 14:48:49 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2020-03-15 08:30:40 +0100 |
| commit | 470f5e063535f91ce0e95798d4aaadfefffb89e0 (patch) | |
| tree | f3dbdc7a04253530c442991821906472de2dbd13 /dev | |
| parent | 4b694f8a641344875b9076670bc8009476fba4aa (diff) | |
Use quotes when "necessary" in the coqtop argument window.
This is at least to be able to use spaces in file names (#11595).
In practice it protects also \, ', ", and many other symbols.
Diffstat (limited to 'dev')
0 files changed, 0 insertions, 0 deletions