diff --git a/Lake/Config/Package.lean b/Lake/Config/Package.lean index bb5e39fa55..742a7f5883 100644 --- a/Lake/Config/Package.lean +++ b/Lake/Config/Package.lean @@ -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. -/ diff --git a/Lake/Config/Resolve.lean b/Lake/Config/Resolve.lean index 59434a1f1d..5f24fd9419 100644 --- a/Lake/Config/Resolve.lean +++ b/Lake/Config/Resolve.lean @@ -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