max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

doc: fix url to profile.ts source (#10628)

Browse source 
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.
This commit is contained in:
Yuri de Wit 2025-10-07 05:41:04 -07:00 • committed by GitHub
parent ca7e7c4279
commit 5c92ffc64d
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/Lean/Util/Profiler.lean
View file

@ -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