From 560b24f8eab0838fd6e01da8c4373f560020aadd Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Sat, 7 Jun 2014 17:04:56 +0200 Subject: Moving a Thread.yield in check_interrupt. --- dev/printers.mllib | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'dev') diff --git a/dev/printers.mllib b/dev/printers.mllib index d9f4aaccec..29eae1620a 100644 --- a/dev/printers.mllib +++ b/dev/printers.mllib @@ -12,12 +12,12 @@ Option Store Exninfo Backtrace -Control IStream Pp_control Loc Compat Flags +Control Pp Segmenttree Unicodetable -- cgit v1.2.3