--- a/src/Pure/General/graph.scala Mon Oct 24 12:01:36 2016 +0200 +++ b/src/Pure/General/graph.scala Mon Oct 24 12:16:12 2016 +0200 @@ -1,5 +1,4 @@ /* Title: Pure/General/graph.scala - Module: PIDE Author: Makarius Directed graphs.