diff options
| author | Théo Zimmermann | 2018-08-03 12:40:58 +0200 |
|---|---|---|
| committer | Théo Zimmermann | 2018-08-31 17:11:02 +0200 |
| commit | ddce09aa86e469676eefb21dccac3f09284c0e0c (patch) | |
| tree | 00d76033871f90e32a10066efcc4a1ff9f8946b9 /kernel/indtypes.ml | |
| parent | 8bcdcb34fa08acaef48be685232b7402495e7ac7 (diff) | |
Trying to make the code of conduct shorter and more to the point.
Diffstat (limited to 'kernel/indtypes.ml')
0 files changed, 0 insertions, 0 deletions