diff options
author | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-03-05 21:47:12 +0100 |
---|---|---|
committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-03-05 21:47:12 +0100 |
commit | f8b624f7bec0406258eee4e08b0cec8d756da6ff (patch) | |
tree | 874c450f7d350455884d409bcfe6bafa44af7b47 /checker/check.mllib | |
parent | eb0feed6d22c11c44e7091c64ce5b1c9d5af987a (diff) | |
parent | 32baedf7a3aebb96f7dd2c7d90a1aef40ed93792 (diff) |
Merge branch 'v8.5'
Diffstat (limited to 'checker/check.mllib')
-rw-r--r-- | checker/check.mllib | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/checker/check.mllib b/checker/check.mllib index 3725989e8..900cfe0c8 100644 --- a/checker/check.mllib +++ b/checker/check.mllib @@ -33,7 +33,7 @@ CStack Util Ppstyle Errors -Ephemeron +CEphemeron Future CUnix |