diff options
| author | Pierre Weis <Pierre.Weis@inria.fr> | 2000-02-15 10:09:55 +0000 |
|---|---|---|
| committer | Pierre Weis <Pierre.Weis@inria.fr> | 2000-02-15 10:09:55 +0000 |
| commit | 2fe1f4d4a015ba07268ba2df584d62f522ec2404 (patch) | |
| tree | 7ece0870d74759a4fa4834b3d1150c8d073253b0 /otherlibs/labltk/browser/shell.ml | |
| parent | 3c173951eca67779ce53f9ec036a76f6bf82451f (diff) | |
Incorporation des améliorations de la dernière version de ocamltk41.
git-svn-id: http://caml.inria.fr/svn/ocaml/trunk@2818 f963ae5c-01c2-4b8c-9fe0-0dff7051ff02
Diffstat (limited to 'otherlibs/labltk/browser/shell.ml')
| -rw-r--r-- | otherlibs/labltk/browser/shell.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/otherlibs/labltk/browser/shell.ml b/otherlibs/labltk/browser/shell.ml index 3a5958806..f63388754 100644 --- a/otherlibs/labltk/browser/shell.ml +++ b/otherlibs/labltk/browser/shell.ml @@ -92,7 +92,7 @@ object (self) Fileevent.remove_fileinput fd:in1; Fileevent.remove_fileinput fd:err1; Unix.kill :pid signal:Sys.sigkill; - Unix.waitpid mode:[] pid; () + ignore (Unix.waitpid mode:[] pid) end with _ -> () end @@ -210,7 +210,7 @@ object (self) Text.mark_set textw mark:"input" index:(`Mark"insert",[`Char(-1)]) end; Mutex.unlock imutex; - ignore (Timer.add ms:100 callback:read_buffer) + Timer.set ms:100 callback:read_buffer in read_buffer () end else begin |