diff options
| author | Hugo Herbelin | 2018-04-06 16:32:36 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2018-05-12 14:56:47 +0200 |
| commit | 556bcae1d29707b21a527a134d38a94623abf5dd (patch) | |
| tree | 86ada5bd96229f1f6d1e6b2469b822c99240d1a8 /kernel/type_errors.ml | |
| parent | 7dd881fc72d62eb0c1f1e5063eb3a8ed268fb5d5 (diff) | |
Sphinx: a "QUICK=1" option to bypass recompilation of the library.
Diffstat (limited to 'kernel/type_errors.ml')
0 files changed, 0 insertions, 0 deletions