Skip to content

Commit dedcfd2

Browse files
authored
Update comment to reflect new profile.js source link
1 parent dfd3d18 commit dedcfd2

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)