# HG changeset patch # User wenzelm # Date 1406214806 -7200 # Node ID e7fe592ee089357e596cd6249acdb077b985e21a # Parent 10df45dd14da62833df926b93f65df563eab6bd5 proper perl; diff -r 10df45dd14da -r e7fe592ee089 Admin/lib/Tools/makedist --- a/Admin/lib/Tools/makedist Thu Jul 24 17:11:40 2014 +0200 +++ b/Admin/lib/Tools/makedist Thu Jul 24 17:13:26 2014 +0200 @@ -157,8 +157,8 @@ fi perl -pi \ - -e "s,val is_identified = false,val is_identified = true,g" \ - -e "s,val is_official = false,val is_official = ${IS_OFFICIAL},g" \ + -e "s,val is_identified = false,val is_identified = true,g;" \ + -e "s,val is_official = false,val is_official = ${IS_OFFICIAL},g;" \ src/Pure/ROOT.ML src/Pure/ROOT.scala perl -pi -e "s,ISABELLE_ID=\"\",ISABELLE_ID=\"$IDENT\",g" lib/scripts/getsettings