refactor: remove unused branch parameter from Source.git

This commit is contained in:
tydeu 2021-12-02 21:25:53 -05:00
parent 1284616296
commit a7a980c12d
2 changed files with 5 additions and 6 deletions

View file

@ -54,7 +54,7 @@ In Lake, dependency sources currently come into flavors:
-/
inductive Source where
| path (dir : FilePath) : Source
| git (url rev : String) (branch : Option String := none) : Source
| git (url rev : String) : Source
deriving Inhabited, Repr
/-- A `Dependency` of a package. -/

View file

@ -16,11 +16,10 @@ Materializes a Git package in the given `dir`,
cloning and/or updating it as necessary.
-/
def materializeGit
(name : String) (dir : FilePath) (url rev : String) (branch : Option String)
(name : String) (dir : FilePath) (url rev : String)
: (LogT IO) Unit := do
if ← dir.isDir then
let br := match branch with | none => "" | some br => "@" ++ br
logInfo s!"{name}: trying to update {dir} to revision {rev}{br}"
logInfo s!"{name}: trying to update {dir} to revision {rev}"
let hash ← parseOriginRevision rev dir
unless ← revisionExists hash dir do fetch dir
checkoutDetach hash dir
@ -37,10 +36,10 @@ downloading and/or updating it as necessary.
def materializeDep (pkg : Package) (dep : Dependency) : (LogT IO) FilePath :=
match dep.src with
| Source.path dir => pkg.dir / dir
| Source.git url rev branch => do
| Source.git url rev => do
let name := dep.name.toString (escape := false)
let depDir := pkg.depsDir / name
materializeGit name depDir url rev branch
materializeGit name depDir url rev
depDir
/--