Skip to content

Commit 83af7d5

Browse files
committed
fix
1 parent 2e93876 commit 83af7d5

File tree

2 files changed

+3
-2
lines changed

2 files changed

+3
-2
lines changed

REPL.lean

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,5 @@
11
import REPL.Frontend
22
import REPL.Lean.InfoTree
3-
import REPL.JSON
3+
import REPL.JSON.REPL
4+
import REPL.JSON.Types
45
import REPL.Main

REPL/JSON/REPL.lean

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,5 @@
11
import REPL.Main
2-
import REPL.Json.Types
2+
import REPL.JSON.Types
33

44
namespace REPL
55

0 commit comments

Comments
 (0)