Mercurial Mercurial > repos > isabelle / comparison
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Admin/makedist
changeset 33910 bae240a8bfe9
parent 33909 24a9d433eb7f
child 33950 0a77b979e593
equal deleted inserted replaced
33909:24a9d433eb7f 33910:bae240a8bfe9 
    91 echo "###"
 
    91 echo "###"
 
    92 
    92 
    93 { wget -q "$REPOS/archive/${VERSION}.tar.gz" -O- | tar -xzf -; } || \
 
    93 { wget -q "$REPOS/archive/${VERSION}.tar.gz" -O- | tar -xzf -; } || \
 
    94   fail "Failed to retrieve $VERSION"
 
    94   fail "Failed to retrieve $VERSION"
 
    95 
    95 
    96 IDENT=$(echo * | sed 's/${REPOS_NAME}-//')
 
    96 IDENT=$(echo * | sed "s/${REPOS_NAME}-//")
 
    97 
    97 
    98 rm -f "${REPOS_NAME}-${IDENT}/.hg_archival.txt"
 
    98 rm -f "${REPOS_NAME}-${IDENT}/.hg_archival.txt"
 
    99 rm -f "${REPOS_NAME}-${IDENT}/.hgtags"
 
    99 rm -f "${REPOS_NAME}-${IDENT}/.hgtags"
 
   100 rm -f "${REPOS_NAME}-${IDENT}/.hgignore"
 
   100 rm -f "${REPOS_NAME}-${IDENT}/.hgignore"
 
   101 rm -f "${REPOS_NAME}-${IDENT}/README_REPOSITORY"
 
   101 rm -f "${REPOS_NAME}-${IDENT}/README_REPOSITORY"
isabelle