> There was a long debate between March and May on the respective merits of the two choices, and IMO we collectively took a very balanced decision.
Oh, OK then. I must have missed that.
But still, I would like to point out that one may need to launch multiple gretls (as I often do for years) and being asked this question each time can be a bit annoying. It is probably rare that here one would answer "no, it was by mistake" Besides, it is not like we are deleting files or doing a system wide change or anything.