diff options
| author | Iavor S. Diatchki <diatchki@galois.com> | 2008-09-05 14:49:21 -0700 |
|---|---|---|
| committer | Iavor S. Diatchki <diatchki@galois.com> | 2008-09-05 14:49:21 -0700 |
| commit | e3666facbb2d60576d8a4f8c6b068d12565f6643 (patch) | |
| tree | f90cd9eb7438477ec1c2a1ff0bab1d535fb4a7fd /.gitignore | |
| parent | c2fa80a0ec94541f9671f16676aeeca2cb79f988 (diff) | |
Make parsing parameters case insensitive.
Thanks to Nicolas Pouillard for reporting this, and sending us a patch.
Diffstat (limited to '.gitignore')
0 files changed, 0 insertions, 0 deletions