Skip to content

Commit

Permalink
typo
Browse files Browse the repository at this point in the history
  • Loading branch information
joneugster committed Feb 11, 2025
1 parent 38d78d6 commit bc050ab
Showing 1 changed file with 2 additions and 2 deletions.
4 changes: 2 additions & 2 deletions Cache/Hashing.lean
Original file line number Diff line number Diff line change
Expand Up @@ -78,9 +78,9 @@ Computes the root hash, which mixes the hashes of the content of:
* `lakefile.lean`
* `lean-toolchain`
* `lake-manifest.json`
and the hash of `Lean.gitHash`.
and the hash of `Lean.githash`.
(We hash `Lean.gitHash` in case the toolchain changes even though `lean-toolchain` hasn't.
(We hash `Lean.githash` in case the toolchain changes even though `lean-toolchain` hasn't.
This happens with the `lean-pr-testing-NNNN` toolchains when Lean 4 PRs are updated.)
-/
def getRootHash : CacheM UInt64 := do
Expand Down

0 comments on commit bc050ab

Please sign in to comment.