diff options
| author | Gregory Malecha | 2015-06-24 09:30:31 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2015-06-24 13:30:33 +0200 |
| commit | 1343b69221ce3eeb3154732e73bbdc0044b224a8 (patch) | |
| tree | 9db5283af41912c241970a5346784df98f4cb917 /lib/flags.ml | |
| parent | d3dabb87cace5a020bc11f6026a371b0cc86d7e9 (diff) | |
Add a space in cast since cast binds loosely.
Fixes bug 3936
This closes #73
Diffstat (limited to 'lib/flags.ml')
0 files changed, 0 insertions, 0 deletions