equal
deleted
inserted
replaced
122 fi |
122 fi |
123 |
123 |
124 $FIND . -name CVS -print | xargs rm -rf |
124 $FIND . -name CVS -print | xargs rm -rf |
125 $FIND . -name .cvsignore -print | xargs rm -rf |
125 $FIND . -name .cvsignore -print | xargs rm -rf |
126 $FIND . "(" -name \*.thy -o -name \*.ML ")" -perm +111 -print | xargs chmod -x |
126 $FIND . "(" -name \*.thy -o -name \*.ML ")" -perm +111 -print | xargs chmod -x |
|
127 $FIND . -print | xargs chmod u+rw |
127 |
128 |
128 |
129 |
129 # build docs |
130 # build docs |
130 |
131 |
131 echo "###" |
132 echo "###" |