aboutsummaryrefslogtreecommitdiff
path: root/dev/db
diff options
context:
space:
mode:
authordesmettr2002-06-20 17:50:42 +0000
committerdesmettr2002-06-20 17:50:42 +0000
commit67c75fa01adbbe1d4e39eff2b930ad168510072c (patch)
treefd320590778df08ae0c810afeaebf977cd5b8287 /dev/db
parentfa430e9d35197b57e267dc0ce965e62dcf8a699f (diff)
*** empty log message ***
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2800 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'dev/db')
0 files changed, 0 insertions, 0 deletions