etc/components
changeset 59480 61d6d5cbbcd3
parent 57436 995f7ebd50ae
child 59810 e749a0f2f401
--- a/etc/components	Thu Feb 05 13:01:12 2015 +0100
+++ b/etc/components	Thu Feb 05 13:01:12 2015 +0100
@@ -1,5 +1,4 @@
 #hard-wired components
-src/Tools/Code
 src/Tools/jEdit
 src/Tools/Graphview
 src/HOL/Mirabelle