aboutsummaryrefslogtreecommitdiffstats
path: root/scheduling/BTLaux.ml
diff options
context:
space:
mode:
Diffstat (limited to 'scheduling/BTLaux.ml')
-rw-r--r--scheduling/BTLaux.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/scheduling/BTLaux.ml b/scheduling/BTLaux.ml
index e8e355b1..863afdf0 100644
--- a/scheduling/BTLaux.ml
+++ b/scheduling/BTLaux.ml
@@ -1,3 +1,3 @@
type inst_info = { mutable inumb : int; mutable pcond : bool option }
-type block_info = { mutable bnumb : int }
+type block_info = { mutable bnumb : int; mutable visited: bool }