chore: cleanup
This commit is contained in:
parent
a7a980c12d
commit
fcc3e3d93e
2 changed files with 3 additions and 4 deletions
|
|
@ -53,8 +53,8 @@ In Lake, dependency sources currently come into flavors:
|
|||
into the packages's `depsDir`.
|
||||
-/
|
||||
inductive Source where
|
||||
| path (dir : FilePath) : Source
|
||||
| git (url rev : String) : Source
|
||||
| path (dir : FilePath)
|
||||
| git (url rev : String)
|
||||
deriving Inhabited, Repr
|
||||
|
||||
/-- A `Dependency` of a package. -/
|
||||
|
|
|
|||
|
|
@ -16,8 +16,7 @@ Materializes a Git package in the given `dir`,
|
|||
cloning and/or updating it as necessary.
|
||||
-/
|
||||
def materializeGit
|
||||
(name : String) (dir : FilePath) (url rev : String)
|
||||
: (LogT IO) Unit := do
|
||||
(name : String) (dir : FilePath) (url rev : String) : (LogT IO) PUnit := do
|
||||
if ← dir.isDir then
|
||||
logInfo s!"{name}: trying to update {dir} to revision {rev}"
|
||||
let hash ← parseOriginRevision rev dir
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue