src/Pure/PIDE/resources.scala
changeset 63020 02921dcc42c3
parent 62556 c115e69f457f
child 63579 73939a9b70a3
     1.1 --- a/src/Pure/PIDE/resources.scala	Mon Apr 18 20:24:19 2016 +0200
     1.2 +++ b/src/Pure/PIDE/resources.scala	Mon Apr 18 20:43:37 2016 +0200
     1.3 @@ -103,7 +103,7 @@
     1.4  
     1.5          val imports =
     1.6            header.imports.map({ case (s, pos) => (import_name(qualifier, node_name, s), pos) })
     1.7 -        Document.Node.Header(imports, header.keywords, Nil)
     1.8 +        Document.Node.Header(imports, header.keywords)
     1.9        }
    1.10        catch { case exn: Throwable => Document.Node.bad_header(Exn.message(exn)) }
    1.11      }