Skip to content

Commit

Permalink
chore: lake: fix typo in materialize error (leanprover#6250)
Browse files Browse the repository at this point in the history
  • Loading branch information
tydeu authored Nov 29, 2024
1 parent 5c7e027 commit c9ee66f
Showing 1 changed file with 1 addition and 1 deletion.
2 changes: 1 addition & 1 deletion src/lake/Lake/Load/Materialize.lean
Original file line number Diff line number Diff line change
Expand Up @@ -148,7 +148,7 @@ def Dependency.materialize
if ver.startsWith "git#" then
return ver.drop 4
else
error s!"{dep.name}: unsupported dependency version format '{ver}' (should be \"git#>rev>\")"
error s!"{dep.name}: unsupported dependency version format '{ver}' (should be \"git#<rev>\")"
let depName := dep.name.toString (escape := false)
let pkg ←
match (← Reservoir.fetchPkg? lakeEnv dep.scope depName |>.toLogT) with
Expand Down

0 comments on commit c9ee66f

Please sign in to comment.