diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2017-08-24 17:14:20 +0200 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2017-09-12 20:38:44 +0200 |
| commit | b9106a956c32e1352fcad5f0138a4e3ddee0474c (patch) | |
| tree | f45611447003783c5cc5dde40c3a0e268b08325d /tools/coqdep_boot.ml | |
| parent | 86b9e40c2e2fd29c747a9f3ad20ebb2701210155 (diff) | |
Fixing bug #5693 (treating empty notation format as any format).
A trick in counting spaces in a format was making the empty notation
not behaving correctly.
Diffstat (limited to 'tools/coqdep_boot.ml')
0 files changed, 0 insertions, 0 deletions