diff options
| author | Théo Zimmermann | 2019-05-24 22:20:02 +0200 |
|---|---|---|
| committer | Théo Zimmermann | 2019-05-24 22:20:02 +0200 |
| commit | e3df4fce6ec981140bbba5f6ac46292dad215754 (patch) | |
| tree | 81d665c50e18438c58f373d6ff742d4acbea48e0 /checker/checkTypes.mli | |
| parent | 7c12318da313191adfa2005f24a77ddc4ad7a062 (diff) | |
Add SUPPORT.md file.
A link to this file will be displayed when people start opening an
issue, and maybe in some other places.
See also:
https://help.github.com/en/articles/adding-support-resources-to-your-project
Diffstat (limited to 'checker/checkTypes.mli')
0 files changed, 0 insertions, 0 deletions