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 /vernac/topfmt.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 'vernac/topfmt.ml')
0 files changed, 0 insertions, 0 deletions