You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
Original bug ID: 787 Reporter: administrator Status: acknowledged Resolution: open Priority: normal Severity: feature Category: otherlibs
Bug description
La fonction suivante me serait extrêmement utile :
Event.timeout : float -> 'a -> 'a event
Avec le fonctionnement suivant : l'évènement (Event.timeout heure
constante) bloque s'il est sélectionné avant heure (au sens
d'Unix.gettimeofday), et retourne immédiatement constante après.
Voilà. Merci encore pour cet excellent langage, et bonne année.
-----BEGIN PGP SIGNATURE-----
Version: GnuPG v1.0.5 (SunOS)
Comment: Pour information voir http://www.gnupg.org
This issue has been open one year with no activity. Consequently, it is being marked with the "stale" label. What this means is that the issue will be automatically closed in 30 days unless more comments are added or the "stale" label is removed. Comments that provide new information on the issue are especially welcome: is it still reproducible? did it appear in other contexts? how critical is it? etc.
Original bug ID: 787
Reporter: administrator
Status: acknowledged
Resolution: open
Priority: normal
Severity: feature
Category: otherlibs
Bug description
La fonction suivante me serait extrêmement utile :
Avec le fonctionnement suivant : l'évènement (Event.timeout heure
constante) bloque s'il est sélectionné avant heure (au sens
d'Unix.gettimeofday), et retourne immédiatement constante après.
Voilà. Merci encore pour cet excellent langage, et bonne année.
-----BEGIN PGP SIGNATURE-----
Version: GnuPG v1.0.5 (SunOS)
Comment: Pour information voir http://www.gnupg.org
iD8DBQE8PCEusGPZlzblTJMRAoQ9AJ4s8nJ6tA/KBz4KW7hSX0bHmae6MgCgl/89
0+ChNVdRXImUtosgkG+ke90=
=mrSJ
-----END PGP SIGNATURE-----
The text was updated successfully, but these errors were encountered: