changeset 77772 | 7e0d920b4e6e |
parent 77028 | f5896dea6fce |
child 78021 | ce6e3bc34343 |
--- a/src/Pure/PIDE/markup.ML Sat Apr 01 14:50:43 2023 +0200 +++ b/src/Pure/PIDE/markup.ML Sat Apr 01 14:59:42 2023 +0200 @@ -674,7 +674,7 @@ (case (Properties.get props fileN, Properties.get props offsetN, Properties.get props nameN) of (SOME file, SOME offset, SOME name) => SOME ({file = file, offset = Value.parse_int offset, name = name}, - Properties.seconds props elapsedN) + Properties.get_seconds props elapsedN) | _ => NONE);