I was definitely not proposing subdirectories of ex. Rather I was proposing multiple directories, if there are enough related items to make a meaningful collection.
Larry > On 31 May 2020, at 22:52, Makarius <[email protected]> wrote: > >> >> Conceivably it could be subdivided, as it seems to have 94 entries. > > Now might be actually a good time to disallow sub-directories of a session > directory. They have accumulated a lot of confusion and problems in the past > decades. _______________________________________________ isabelle-dev mailing list [email protected] https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
