Admin/makedist
changeset 32361 141e5151b918
parent 31842 af5221147455
child 33844 813b091dd63b
equal deleted inserted replaced
32360:79b5b3031c87 32361:141e5151b918
   163 fi
   163 fi
   164 
   164 
   165 perl -pi -e "s,val changelog = \"\",val changelog = \"$REPOS/log/$IDENT\",g" src/Pure/ROOT.ML
   165 perl -pi -e "s,val changelog = \"\",val changelog = \"$REPOS/log/$IDENT\",g" src/Pure/ROOT.ML
   166 perl -pi -e "s,ISABELLE_IDENTIFIER=\"\",ISABELLE_IDENTIFIER=\"$DISTNAME\",g" lib/scripts/getsettings
   166 perl -pi -e "s,ISABELLE_IDENTIFIER=\"\",ISABELLE_IDENTIFIER=\"$DISTNAME\",g" lib/scripts/getsettings
   167 perl -pi -e "s,{ISABELLE},$DISTNAME,g" lib/html/library_index_header.template
   167 perl -pi -e "s,{ISABELLE},$DISTNAME,g" lib/html/library_index_header.template
   168 perl -pi -e "s,Isabelle repository version,$DISTVERSION,g" src/Pure/ROOT.ML lib/Tools/version
   168 perl -pi -e "s,unidentified repository version,$DISTVERSION,g" src/Pure/ROOT.ML lib/Tools/version
   169 perl -pi -e "s,the internal repository version of Isabelle,$DISTVERSION,g" README
   169 perl -pi -e "s,some unidentified repository version of Isabelle,$DISTVERSION,g" README
   170 
   170 
   171 
   171 
   172 # create archives
   172 # create archives
   173 
   173 
   174 echo "###"
   174 echo "###"