diff --git a/src/runtime/io.cpp b/src/runtime/io.cpp index b9c34e9bb7..24da3eb136 100644 --- a/src/runtime/io.cpp +++ b/src/runtime/io.cpp @@ -15,6 +15,9 @@ Author: Leonardo de Moura #include // NOLINT #include #endif +#ifndef LEAN_WINDOWS +#include +#endif #include #include #include @@ -653,6 +656,10 @@ void initialize_io() { mark_persistent(g_stream_stderr); g_stream_stdin = lean_stream_of_handle(io_wrap_handle(stdin)); mark_persistent(g_stream_stdin); +#ifndef LEAN_WINDOWS + // We want to handle SIGPIPE ourselves + lean_always_assert(signal(SIGPIPE, SIG_IGN) != SIG_ERR); +#endif } void finalize_io() { diff --git a/tests/lean/Process.lean b/tests/lean/Process.lean index 601f314019..05f3e1b6ba 100644 --- a/tests/lean/Process.lean +++ b/tests/lean/Process.lean @@ -15,3 +15,9 @@ open IO.Process child.stdin.flush; child.wait; child.stdout.readToEnd + +#eval do + child ← spawn { cmd := "true", stdin := Stdio.piped }; + child.wait; + child.stdin.putStrLn "ha!"; + child.stdin.flush <|> IO.println "flush of broken pipe failed" diff --git a/tests/lean/Process.lean.expected.out b/tests/lean/Process.lean.expected.out index 2ed42fbab4..bce17e82fc 100644 --- a/tests/lean/Process.lean.expected.out +++ b/tests/lean/Process.lean.expected.out @@ -2,3 +2,4 @@ hi! 0 "ho!\n" "hu!\n" +flush of broken pipe failed