diff options
Diffstat (limited to 'otherlibs/labltk/support/timer.ml')
| -rw-r--r-- | otherlibs/labltk/support/timer.ml | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/otherlibs/labltk/support/timer.ml b/otherlibs/labltk/support/timer.ml index 9bae936344..349bf6a2e3 100644 --- a/otherlibs/labltk/support/timer.ml +++ b/otherlibs/labltk/support/timer.ml @@ -16,6 +16,7 @@ (* $Id$ *) (* Timers *) +open Support open Protocol type tkTimer = int @@ -33,7 +34,7 @@ let add ~ms ~callback = let wrapped _ = clear_callback id; (* do it first in case f raises exception *) callback() in - Hashtbl.add' callback_naming_table ~key:id ~data:wrapped; + Hashtbl'.add callback_naming_table ~key:id ~data:wrapped; if !Protocol.debug then begin prerr_cbid id; prerr_endline " for timer" end; |