aboutsummaryrefslogtreecommitdiffstats
path: root/scheduling
diff options
context:
space:
mode:
Diffstat (limited to 'scheduling')
-rw-r--r--scheduling/BTLScheduleraux.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/scheduling/BTLScheduleraux.ml b/scheduling/BTLScheduleraux.ml
index 75672243..0e682c4c 100644
--- a/scheduling/BTLScheduleraux.ml
+++ b/scheduling/BTLScheduleraux.ml
@@ -272,7 +272,7 @@ let schedule_blk n ibf btl =
| None -> btl
let turn_all_loads_nontrap n ibf btl =
- if not !config.has_non_trapping_loads then btl
+ if not !config.has_non_trapping_loads || not !Clflags.option_fnontrap_loads then btl
else
let rec traverse_rec ib =
match ib with