diff options
| author | Pierre Letouzey | 2015-12-14 00:33:29 +0100 |
|---|---|---|
| committer | Pierre Letouzey | 2015-12-14 00:33:29 +0100 |
| commit | 123cbdfef1733a1786109bd1b97ccfa3f62c0d1c (patch) | |
| tree | 1233ee2d0712b4f89dbeb2d06c0b6a43b72009e3 /kernel/nativecode.mli | |
| parent | a275da6e67b91d9ccae0a952eb1feab2e122076e (diff) | |
Extraction: cleanup a hack (Pp.is_empty instead of Failure "empty phrase")
Diffstat (limited to 'kernel/nativecode.mli')
0 files changed, 0 insertions, 0 deletions