author | wenzelm |
Wed, 20 Jan 2021 21:42:04 +0100 | |
changeset 73166 | 78dd1abfbbe1 |
parent 73165 | 1004cb57d502 |
child 73167 | 490ca65ecae2 |
--- a/src/Pure/System/options.scala Wed Jan 20 21:18:40 2021 +0100 +++ b/src/Pure/System/options.scala Wed Jan 20 21:42:04 2021 +0100 @@ -120,7 +120,7 @@ case bad => error(bad.toString) } try { (options.set_section("") /: ops) { case (opts, op) => op(opts) } } - catch { case ERROR(msg) => error(msg + Position.File(file_name)) } + catch { case ERROR(msg) => error(msg + Position.here(Position.File(file_name))) } } def parse_prefs(options: Options, content: String): Options =