refactor(library/debugger): move debugger to tools

2016-12-17 10:50:13 -08:00 · 2016-12-17 10:50:13 -08:00 · 305838bece
commit 305838bece
parent 63ec7cd6cf
4 changed files with 3 additions and 3 deletions
--- a/library/tools/debugger/cli.lean
+++ b/library/tools/debugger/cli.lean
@ -5,7 +5,7 @@ Authors: Leonardo de Moura

 Simple command line interface for debugging Lean programs and tactics.
 -/
-import debugger.util
+import tools.debugger.util

 namespace debugger

--- a/library/tools/debugger/default.lean
+++ b/library/tools/debugger/default.lean
@ -3,4 +3,4 @@ Copyright (c) 2016 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
-import debugger.util debugger.cli
+import tools.debugger.util tools.debugger.cli
--- a/library/tools/debugger/util.lean
+++ b/library/tools/debugger/util.lean
--- a/tmp/debugger_example.lean
+++ b/tmp/debugger_example.lean
@ -1,4 +1,4 @@
-import debugger
+import tools.debugger

 set_option debugger true
 set_option debugger.autorun true