changeset 69366 | b6dacf6eabe3 |
parent 68224 | 1f7308050349 |
child 69367 | 34b7550b66c7 |
--- a/src/Pure/Tools/spell_checker.scala Wed Nov 28 15:38:18 2018 +0100 +++ b/src/Pure/Tools/spell_checker.scala Wed Nov 28 16:14:31 2018 +0100 @@ -66,7 +66,7 @@ class Dictionary private[Spell_Checker](val path: Path) { - val lang = path.split_ext._1.base_name + val lang = path.split_ext._1.file_name val user_path = Path.explode("$ISABELLE_HOME_USER/dictionaries") + Path.basic(lang) override def toString: String = lang }