X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=blobdiff_plain;f=CVSROOT%2Fmodules;fp=CVSROOT%2Fmodules;h=0000000000000000000000000000000000000000;hp=cb9e9efc94b342879a5fff24b425473fc11edd01;hb=869549224eef6278a48c16ae27dd786376082b38;hpb=89262281b6e83bd2321150f81f1a0583645eb0c8

diff --git a/CVSROOT/modules b/CVSROOT/modules
deleted file mode 100644
index cb9e9efc9..000000000
--- a/CVSROOT/modules
+++ /dev/null
@@ -1,26 +0,0 @@
-# Three different line formats are valid:
-#	key	-a    aliases...
-#	key [options] directory
-#	key [options] directory files...
-#
-# Where "options" are composed of:
-#	-i prog		Run "prog" on "cvs commit" from top-level of module.
-#	-o prog		Run "prog" on "cvs checkout" of module.
-#	-e prog		Run "prog" on "cvs export" of module.
-#	-t prog		Run "prog" on "cvs rtag" of module.
-#	-u prog		Run "prog" on "cvs update" of module.
-#	-d dir		Place module in directory "dir" instead of module name.
-#	-l		Top-level directory only -- do not recurse.
-#
-# NOTE:  If you change any of the "Run" options above, you'll have to
-# release and re-checkout any working directories of these modules.
-#
-# And "directory" is a path to a directory relative to $CVSROOT.
-#
-# The "-a" option specifies an alias.  An alias is interpreted as if
-# everything on the right of the "-a" had been typed on the command line.
-#
-# You can encode a module within a module by using the special '&'
-# character to interpose another module into the current module.  This
-# can be useful for creating a module that consists of many directories
-# spread out over the entire source repository.