Hi there,
a slight oddity when using "isabelle build" with "-d ." inside
$ISABELLE_HOME is that the build process is aborted with the message
Duplicate session "RAW" (file src/Pure/ROOT)
My guess is that this is due to a clash between the default ROOTS
location $ISABELLE_HOME and the explicitly provided "." (which points to
the same directory).
Wouldn't it make sense to just ignore -d options that are adding session
directories which are already there.
If this is not feasible, how about emitting some appropriate message
(i.e., which gives the user a hint that he might have problems since he
tried to add a session directory that was already taken into account) in
addition to "Duplicate sessions ..." and/or mentioning this point in the
documentation of the "-d" flag?
cheers
chris
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
