On Sat, Aug 23, 2014 at 09:33:56AM -0400, Stefan Monnier wrote: > > Yes, you can configure such behaviour. > > I already have plenty of ways to configure the behavior I need. > This discussion is about the default behavior. Exactly. I hope the reasoning behind current defaults has been explained adequately.
That said, it would be great to improve reporting if something like this happens. Hopefully with #755581 fixed, emergency mode will be entered successfully. Zbyszek -- To UNSUBSCRIBE, email to [email protected] with a subject of "unsubscribe". Trouble? Contact [email protected]
