From 5c92ffc64d66d9d6adf32c279c79ebb39fdccdda Mon Sep 17 00:00:00 2001 From: Yuri de Wit Date: Tue, 7 Oct 2025 05:41:04 -0700 Subject: [PATCH] doc: fix url to profile.ts source (#10628) This PR fixes a broken link to the firefox profile definitions in one of the comments. The `profile.js` file was renamed to `profile.ts` while the rest of the url remained the same. --- src/Lean/Util/Profiler.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) 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