[isabelle-dev] isabelle build: "Duplicate session"

[Christian Sternagel]

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