| changeset 71601 | 97ccf48c2f0c |
| parent 66415 | 96ad7d5ff613 |
| child 75393 | 87ebf5a50283 |
--- a/src/Pure/PIDE/document_id.scala Fri Mar 27 13:04:15 2020 +0100 +++ b/src/Pure/PIDE/document_id.scala Fri Mar 27 22:01:27 2020 +0100 @@ -17,7 +17,7 @@ type Exec = Generic val none: Generic = 0 - val make = Counter.make() + val make: Counter = Counter.make() def apply(id: Generic): String = Value.Long.apply(id) def unapply(s: String): Option[Generic] = Value.Long.unapply(s)