1 files changed, 1 insertions, 11 deletions
diff --git a/configure b/configure
index 25acccb8a..9a002198d 100755
--- a/configure
+++ b/configure
@@ -1030,18 +1030,8 @@ let localwwwrefman = "file:/" ^ docdir ^ "html/refman"
 
 END_OF_COQ_CONFIG
 
-# Subdirectories of theories/ added in coq_config.ml
-# Note: don't propagate output of cd if any: it's verbose when CDPATH is defined
-subdirs () {
-    (cd $1; find * \( -name .svn -prune \) -o \( -type d -exec printf "\"%s\";\n" {} \; \) >> "$mlconfig_file")
-}
-
-echo "let theories_dirs = [" >> "$mlconfig_file"
-subdirs theories
-echo "]" >> "$mlconfig_file"
-
 echo "let plugins_dirs = [" >> "$mlconfig_file"
-subdirs plugins
+find plugins/* \( -name .svn -prune \) -o \( -type d -exec printf "\"%s\";\n" {} \; \) >> "$mlconfig_file"
 echo "]" >> "$mlconfig_file"
 
 chmod a-w "$mlconfig_file"