Pipes in lean on windows

Stream: general

[Keeley Hoek]

Just a quick question for someone in-the-know: does lean lack an implementation of pipes on windows? I'm looking in src/library/pipe.(h/cpp) and it looks empty for windows---am I missing something?

[Keeley Hoek]

I guess since even the windows version is built with MSYS2 it doesn't matter

[Sebastian Ullrich]

See https://github.com/leanprover/lean/blob/0eebde1b8b24b087935b75542a3858715097fff2/src/library/process.cpp#L104