refactor: remove 'build' from Target/Trace/Task file names

This commit is contained in:
tydeu 2021-08-15 19:16:12 -04:00
parent ddf02cb339
commit c8b558a2d1
6 changed files with 5 additions and 5 deletions

View file

@ -5,7 +5,7 @@ Authors: Gabriel Ebner, Sebastian Ullrich, Mac Malone
-/
import Lean.Data.Name
import Lean.Elab.Import
import Lake.BuildTarget
import Lake.Target
import Lake.BuildTop
import Lake.Resolve
import Lake.Package

View file

@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
Authors: Mac Malone
-/
import Lake.Compile
import Lake.BuildTarget
import Lake.Target
open System
namespace Lake

View file

@ -7,7 +7,7 @@ import Lean.Data.Name
import Lean.Elab.Import
import Std.Data.HashMap
import Lake.LeanVersion
import Lake.BuildTarget
import Lake.Target
open Lean Std System

View file

@ -3,8 +3,8 @@ Copyright (c) 2021 Mac Malone. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Mac Malone
-/
import Lake.BuildTask
import Lake.BuildTrace
import Lake.Task
import Lake.Trace
open System
namespace Lake