rename contract-gui.rkt to blueboxes-gui.rkt
This commit is contained in:
parent
d3b4db2ed1
commit
0d92608367
|
@ -48,7 +48,7 @@ If the namespace does not, they are colored the unbound color.
|
||||||
"traversals.rkt"
|
"traversals.rkt"
|
||||||
"annotate.rkt"
|
"annotate.rkt"
|
||||||
"../tooltip.rkt"
|
"../tooltip.rkt"
|
||||||
"contract-gui.rkt")
|
"blueboxes-gui.rkt")
|
||||||
(provide tool@)
|
(provide tool@)
|
||||||
|
|
||||||
(define orig-output-port (current-output-port))
|
(define orig-output-port (current-output-port))
|
||||||
|
|
Loading…
Reference in New Issue
Block a user