Skip to content

Commit 5c92ffc

Browse files
authored
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.
1 parent ca7e7c4 commit 5c92ffc

File tree

1 file changed

+1
-1
lines changed

1 file changed

+1
-1
lines changed

src/Lean/Util/Profiler.lean

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -14,7 +14,7 @@ public section
1414

1515
namespace Lean.Firefox
1616

17-
/-! Definitions from https://github.com/firefox-devtools/profiler/blob/main/src/types/profile.js -/
17+
/-! Definitions from https://github.com/firefox-devtools/profiler/blob/main/src/types/profile.ts -/
1818

1919
structure Milliseconds where
2020
ms : Float

0 commit comments

Comments
 (0)