diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2016-08-26 14:46:33 +0200 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2017-05-13 12:20:52 +0200 |
| commit | e3550a0acc39e235e01a727267b12a7c06f23b2c (patch) | |
| tree | c26897adeffc2377e55517277d49a302eef46ea3 /library/globnames.ml | |
| parent | e3a3b4bb17c40b6af2ef8501c405f0600cc6d65b (diff) | |
Uniformity of style for selecting plural or not; spacing for comma.
Diffstat (limited to 'library/globnames.ml')
0 files changed, 0 insertions, 0 deletions