diff --git a/tools/archive_conf_files.sh b/tools/archive_conf_files.sh new file mode 100644 index 0000000..28b6b24 --- /dev/null +++ b/tools/archive_conf_files.sh @@ -0,0 +1,9 @@ +# Use this script to make an archive of the contents of all +# of the configuration files we edit with editconf.py. +for fn in `grep -hr editconf.py setup | sed "s/tools\/editconf.py //" | sed "s/ .*//" | sort | uniq`; do + echo ====================================================================== + echo $fn + echo ====================================================================== + cat $fn +done +