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