diff options
| author | John MacFarlane <jgm@berkeley.edu> | 2014-11-25 11:23:31 -0800 |
|---|---|---|
| committer | John MacFarlane <jgm@berkeley.edu> | 2014-11-25 11:24:49 -0800 |
| commit | e56cd9e8fa1ed0fbda3bee7eba1b13829ba44082 (patch) | |
| tree | 8ad8b4da4dad2d9ce9da79b78e285db0d49e90a7 /src | |
| parent | 440a56ba2b12e1c5d068ab6d8a5768d7470d5a31 (diff) | |
Don't open shared library if --dump-tests or --debug-normalization.
Diffstat (limited to 'src')
0 files changed, 0 insertions, 0 deletions