# HG changeset patch # User wenzelm # Date 1281381804 -7200 # Node ID fb1b255d6e36a07d1be98059d08fcd001e7e99b9 # Parent 3d4e521014f74484c965fe6cd311e533698ec749 more robust fifo rendezvous: Cygwin 1.7 does not really block as expected; diff -r 3d4e521014f7 -r fb1b255d6e36 src/Pure/System/isabelle_process.ML --- a/src/Pure/System/isabelle_process.ML Mon Aug 09 18:18:32 2010 +0200 +++ b/src/Pure/System/isabelle_process.ML Mon Aug 09 21:23:24 2010 +0200 @@ -63,8 +63,10 @@ fun rendezvous f fifo = let val path = File.platform_path (Path.explode fifo); - val result = f fifo; (*block until peer is ready*) - val _ = OS.FileSys.remove path; (*ready; prevent future access -- potential race condition*) + val result = f fifo; (*should block until peer is ready*) + val _ = + if String.isSuffix "cygwin" ml_platform then () (*Cygwin 1.7: no proper blocking on open*) + else OS.FileSys.remove path; (*prevent future access*) in result end; in