diff options
author | Bernhard Schommer <bernhardschommer@gmail.com> | 2019-07-09 14:31:21 +0200 |
---|---|---|
committer | Xavier Leroy <xavierleroy@users.noreply.github.com> | 2019-07-10 10:56:45 +0200 |
commit | fcbd9addf6f8c10822294dc397d13af10b9d52f2 (patch) | |
tree | 6da064afba49677dd05dee282e6abb3fa2cf7fe3 /tools/modorder.ml | |
parent | 026d8bf506a0a4afebe4e41ad5ce2e7523c45ffc (diff) | |
download | compcert-fcbd9addf6f8c10822294dc397d13af10b9d52f2.tar.gz compcert-fcbd9addf6f8c10822294dc397d13af10b9d52f2.zip |
Change condition for warning of conditional expr
The warning should only be active if the optimization is active,
so the check is only performed when the warning is active and
additionally the command line flag -Obranchless is specified.
Diffstat (limited to 'tools/modorder.ml')
0 files changed, 0 insertions, 0 deletions