[isabelle-dev] isabelle build: "Duplicate session"
c-sterna at jaist.ac.jp
Tue Nov 13 05:03:30 CET 2012
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?
More information about the isabelle-dev