I also want to emphasize again that "using" the repository version is
not the way to get the "lastest features" earlier that everybody else.
It rather means that you somehow participate in the ongoing construction
process in what will become a proper release eventually.
Sure, I know that (although it works quite well for me most of the time ;)).
So it is important to point out omissions or snags, but without any
expectation that it is addressed in real-time. You also need to be
ready to work with half-finished things until the next release.
Absolutely. Of course, I do not want to impose any pressure. Sometimes
it is just hard to know whether some snag was not detected yet or is
already in the pipeline... so I report anything ;).
From an external viewpoint it is often not obvious how much effort is
needed to do some "tiny" change. So please, just bear with us.
Maybe it would be a good idea to collect "feature-requests" in the wiki?
(The official place of collection is currently the mailing list, but it
is not that easy to extract this kind of information.) I mean, in order
to have a place to point like: "first look there and only if you do not
find your 'feature' there, write to the mailing list".
cheers
chris
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
