Admin/Mercurial/hgrc
author haftmann
Wed, 11 Mar 2009 08:45:57 +0100
changeset 30432 aad3cd70e25a
parent 28928 bbc600e2276c
permissions -rw-r--r--
merged
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
27458
f1976a293968 hgrc for conversion and web service;
wenzelm
parents:
diff changeset
     1
[extensions]
f1976a293968 hgrc for conversion and web service;
wenzelm
parents:
diff changeset
     2
hgext.convert =
f1976a293968 hgrc for conversion and web service;
wenzelm
parents:
diff changeset
     3
f1976a293968 hgrc for conversion and web service;
wenzelm
parents:
diff changeset
     4
[convert]
28000
ca56bbb99607 replaced /home/isabelle/html-data/isabelle-repos by /home/isabelle-repository/repos;
wenzelm
parents: 27726
diff changeset
     5
cvsps = /home/isabelle-repository/repos/cvsps-2.1-patched/cvsps -A -u --cvs-direct --norc -b HEAD
27458
f1976a293968 hgrc for conversion and web service;
wenzelm
parents:
diff changeset
     6
f1976a293968 hgrc for conversion and web service;
wenzelm
parents:
diff changeset
     7
[web]
27510
a55484e65b65 style = isabelle (based on gitweb);
wenzelm
parents: 27481
diff changeset
     8
style = isabelle
28928
bbc600e2276c adapted description: old CVS;
wenzelm
parents: 28000
diff changeset
     9
description = Snapshot of the old Isabelle CVS
27458
f1976a293968 hgrc for conversion and web service;
wenzelm
parents:
diff changeset
    10
allow_archive = gz
27479
9bcd25618d0c maxfiles = 50;
wenzelm
parents: 27473
diff changeset
    11
maxfiles = 50