diff options
| author | Gaëtan Gilbert | 2020-07-07 15:19:36 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert | 2020-07-07 15:19:36 +0200 |
| commit | f23ce3f827fa340bfa0ab0b0abfc953a626fcebd (patch) | |
| tree | 592d559c6ac2dd5307f03fe7a800dcdfdd8cbfd9 /dev | |
| parent | 8907a5b7d2b91bff0b573956a05e4679b5238161 (diff) | |
Reindent ppvernac.ml
It used to be a big functor but changed in
8c5adfd5acb883a3bc2850b6fc8c29d352a421f8
The functor indent is now incorrect.
Diffstat (limited to 'dev')
0 files changed, 0 insertions, 0 deletions