Admin/makedist
changeset 7115 37178f53ed4d
parent 6958 2ed4b761d6d5
child 7781 7a8e91b8c100
equal deleted inserted replaced
7114:f1e787b90fdc 7115:37178f53ed4d
   130 mv -f $MOVE Distribution/doc
   130 mv -f $MOVE Distribution/doc
   131 rm Distribution/doc/Isa-logics.eps
   131 rm Distribution/doc/Isa-logics.eps
   132 cp Admin/index.html $DISTBASE
   132 cp Admin/index.html $DISTBASE
   133 rm -rf Admin Doc
   133 rm -rf Admin Doc
   134 
   134 
   135 mkdir src
   135 mkdir src contrib
   136 mv $LOGICS src
   136 mv $LOGICS src
   137 
   137 
   138 mv Distribution/* .
   138 mv Distribution/* .
   139 rmdir Distribution
   139 rmdir Distribution
   140 
   140