diff --git a/src/Lean/Util/Profiler.lean b/src/Lean/Util/Profiler.lean index 69ab11fcf3..999e1b20ef 100644 --- a/src/Lean/Util/Profiler.lean +++ b/src/Lean/Util/Profiler.lean @@ -14,7 +14,7 @@ public section namespace Lean.Firefox -/-! Definitions from https://github.com/firefox-devtools/profiler/blob/main/src/types/profile.js -/ +/-! Definitions from https://github.com/firefox-devtools/profiler/blob/main/src/types/profile.ts -/ structure Milliseconds where ms : Float