aboutsummaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
-rw-r--r--Asmblockdeps.patch2
1 files changed, 1 insertions, 1 deletions
diff --git a/Asmblockdeps.patch b/Asmblockdeps.patch
index c0ee290e..a2d8c7be 100644
--- a/Asmblockdeps.patch
+++ b/Asmblockdeps.patch
@@ -8,7 +8,7 @@
- pure_bblock_simu_test true
+let bblock_simub bb tbb =
+ let nb_instructions = Camlcoq.Z.to_int64 @@ Asmvliw.size bb
-+ in let start_time = (Unix.times ()).Unix.tms_utime
++ in let start_time = (Gc.major(); (Unix.times ()).Unix.tms_utime)
+ in let simub = pure_bblock_simu_test true bb tbb
+ in let refer = ref false
+ in begin