diff options
| author | Jasper Hugunin | 2018-02-22 18:38:24 -0800 |
|---|---|---|
| committer | Jasper Hugunin | 2018-02-22 18:38:24 -0800 |
| commit | 6304640dbd82cf24e2fb8346881223d165acf934 (patch) | |
| tree | 32c2194785166c22122dbd5254a14ebbc2512533 /kernel/type_errors.mli | |
| parent | 0c5f0afffd37582787f79267d9841259095b7edc (diff) | |
Document Arguments extra scopes flag
Diffstat (limited to 'kernel/type_errors.mli')
0 files changed, 0 insertions, 0 deletions