Changes

Summary

permissive Doc.dirs: some entries may be absent due to distribution bootstrap, e.g. $JEDIT_HOME/dist/doc;

Changeset 67604:02cf352cbc4c by wenzelm: permissive Doc.dirs: some entries may be absent due to distribution bootstrap, e.g. $JEDIT_HOME/dist/doc;
The file was modified	`src/Pure/Tools/doc.scala` (diff)