--- a/src/Pure/General/long_name.scala Mon Apr 03 13:39:13 2017 +0200 +++ b/src/Pure/General/long_name.scala Mon Apr 03 14:29:44 2017 +0200 @@ -25,4 +25,3 @@ if (name == "") "" else explode(name).last } -