diff options
| author |  Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-09-25 15:36:15 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-09-25 17:35:49 +0200 |
| commit | 3510612550c32c790447b45ee01efbcf855815b9 (patch) | |
| tree | cece3ce824f636dd5dfca234472a7b90dfc5e2be /vernac/mltop.ml | |
| parent | 4b6383889d4d38de4c9a28bee960b30114a51b16 (diff) | |
[doc] Update INSTALL to match reality.
Diffstat (limited to 'vernac/mltop.ml')
0 files changed, 0 insertions, 0 deletions