<div dir="ltr"><div class="gmail_extra"><br><div class="gmail_quote">On 24 February 2016 at 15:14, Makarius <span dir="ltr"><<a href="mailto:makarius@sketis.net" target="_blank">makarius@sketis.net</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex"><br>
How does this compare to your other Cygwin installation?<span class=""></span></blockquote></div><br></div><div class="gmail_extra">I installed the version from <a href="http://isabelle.in.tum.de/cygwin_2016" rel="noreferrer" target="_blank">http://isabelle.in.tum.de/cygwin_2016</a>, but there was no change in the result, still the same error.<br></div><div class="gmail_extra"><br clear="all"><blockquote style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex" class="gmail_quote">A new process environment is not immediately visible. So "nothing happens" looks like a success.<br></blockquote><div dir="ltr"><br></div><div>I didn't notice that. When I now run both commands and then <span style="font-family:monospace,monospace">echo $?</span><span style="font-family:arial,helvetica,sans-serif"> </span>I get 127 as result both times.<br><br></div><div>Cheers Fabian<br></div></div></div>