diff options
| author | James Fish <james@fishcakez.com> | 2014-11-20 15:57:07 +0000 |
|---|---|---|
| committer | James Fish <james@fishcakez.com> | 2014-11-20 16:05:03 +0000 |
| commit | 16da6d2630d11a8ac9d9c75e3c344415050efac7 (patch) | |
| tree | a3898305079d74a987cb6f14322bc11bf8d92221 /include | |
| parent | a96fddfcde4ab3a71aea01914bd3e7a836db46c0 (diff) | |
Add options to skip updating plt or success typing
* --update-plt=true|false (false skips updating plt)
* --succ-typings=true|false (false skips success typing analysis)
Diffstat (limited to 'include')
0 files changed, 0 insertions, 0 deletions