Comment author: administrator

From: luc.habert@inria.fr
Subject: Unix.select (#3138)
Date: Thu, 10 Jan 2002 13:02:43 +0100 (MET)
Message-ID: 200201101202.NAA13227@pauillac.inria.fr

Full_Name: Luc Habert
Version: 3.04
OS: Linux
Submission from: gargamel.ens.fr (129.199.131.138)

I am experiencing a problem when using Unix.select while the graphics
window is open :

#load "unix.cma";;

#load "graphics.cma";;

Graphics.open_graph "";;

• : unit = ()

Unix.select [] [] [] 1.;;

Exception: Unix.Unix_error (Unix.EINTR, "select", "").

This happens as well in the toplevel as in byte or native compiled
programs.

This is not a bug: the select system call is interrupted by
the Graphics librarie's internal use of interval timer.
The quick workaround is as follows, (though it is not so presice):

let sleep sec =
let start = Unix.gettimeofday () in
let rec delay t =
try Unix.Unix_error(Unix.EINTR, _, _) ->
let now = Unix.gettimeofday () in
let remaining = start +. n -. now in
if remaining > 0.0 then delay remaining
in
delay sec
;;

--
JPF

Comment author: administrator

Acceptable Linux behavior with timer signals