From d741babd4962ff645651bd98706365e05941aae7 Mon Sep 17 00:00:00 2001 From: Sam Westrick Date: Fri, 29 Sep 2023 18:06:34 +0000 Subject: [PATCH] get rid of compilation warnings and remove profiling print --- basis-library/schedulers/hybrid/Scheduler.sml | 9 +++++---- 1 file changed, 5 insertions(+), 4 deletions(-) diff --git a/basis-library/schedulers/hybrid/Scheduler.sml b/basis-library/schedulers/hybrid/Scheduler.sml index 6ed416453..9affb0870 100644 --- a/basis-library/schedulers/hybrid/Scheduler.sml +++ b/basis-library/schedulers/hybrid/Scheduler.sml @@ -877,7 +877,7 @@ struct val result = g () val t1 = timeNowMicrosecondsSinceProgramStart () in - print ("gpu manager exec work elapsed: " ^ Int64.toString (t1-t0) ^ "us\n"); + (* print ("gpu manager exec work elapsed: " ^ Int64.toString (t1-t0) ^ "us\n"); *) result end @@ -1000,7 +1000,7 @@ struct ; (friend, d', SOME holding') ) - | NONE => (bestFriend, bestDepth, holding) + | _ => (bestFriend, bestDepth, holding) ) | _ => (bestFriend, bestDepth, holding) @@ -1069,11 +1069,12 @@ struct else (* tryKeepPendingChoice bf *) case tryKeepPendingChoice bf of - NONE => NONE - | SOME (t as Continuation (_, d)) => + SOME (t as Continuation (_, d)) => if d >= bd then SOME t else if tryPushPendingChoice bf t then NONE else die (fn _ => "scheduler error: push pending back failed\n") + + | _ => NONE end