> > You can contribute indirectly to important reforms that are in the > pipeline for a long time by keeping your sources in a more up-to-date > state.
As you said, there seems to be no other way of achieving what I required. I realized that, added a comment (*Argh!*) expressing my disgust about it, but at the end had to implement the hack in order to get the desired behaviour. Now you just removed the desired behaviour, not having a solution how to get it back ... fortunately, in this particular case, it is not essential, as this thing was inside some rarely used debugging tool. -- Peter > > > Makarius > > ---------------------------------------------------------------------------- > http://stop-ttip.org 777,443 people so far > ---------------------------------------------------------------------------- _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
