fixes

leanprover · Oct 20, 2024 · 471fc6e · 471fc6e
1 parent f837116
commit 471fc6e
Show file tree

Hide file tree

Showing 2 changed files with 2 additions and 1 deletion.
diff --git a/src/lake/Lake/DSL/Targets.lean b/src/lake/Lake/DSL/Targets.lean
@@ -12,6 +12,7 @@ Macros for declaring Lake targets and facets.
 
 namespace Lake.DSL
 open Lean Parser Command
+open System (FilePath)
 
 syntax buildDeclSig :=
   identOrStr (ppSpace simpleBinder)? Term.typeSpec declValSimple

diff --git a/src/lake/examples/targets/lakefile.lean b/src/lake/examples/targets/lakefile.lean
@@ -40,7 +40,7 @@ package_facet print_name pkg : Unit := Job.async do
   IO.println pkg.name
   return ((), .nil)
 
-module_facet get_src mod : FilePath := do
+module_facet get_src mod : System.FilePath := do
   inputTextFile mod.leanFile
 
 module_facet print_src mod : Unit := do