equal
deleted
inserted
replaced
1 [extensions] |
1 [extensions] |
2 hgext.convert = |
2 hgext.convert = |
3 |
3 |
4 [convert] |
4 [convert] |
5 cvsps = /home/isabelle/html-data/isabelle-repos/cvsps-2.1-patched/cvsps -A -u --cvs-direct --norc -b HEAD |
5 cvsps = /home/isabelle-repository/repos/cvsps-2.1-patched/cvsps -A -u --cvs-direct --norc -b HEAD |
6 |
6 |
7 [web] |
7 [web] |
8 style = isabelle |
8 style = isabelle |
9 description = Snapshot of the official Isabelle CVS repository |
9 description = Snapshot of the official Isabelle CVS repository |
10 allow_archive = gz |
10 allow_archive = gz |