diff options
| author | Cyprien Mangin | 2016-09-28 16:56:22 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2016-11-04 11:15:25 +0100 |
| commit | 5939d426ac785ec063e66a302f3692b645993c56 (patch) | |
| tree | 499db9b859620ffcf0fe6bded9cf3dbc572ad382 /kernel/type_errors.ml | |
| parent | 962a5d3526290b83967a92ef1eb772894d10362b (diff) | |
Add documentation for [Set Warnings] and the -w option.
Diffstat (limited to 'kernel/type_errors.ml')
0 files changed, 0 insertions, 0 deletions