diff options
| author |  Samuel Mimram <smimram@debian.org> | 2006-11-23 14:28:36 +0000 |
|---|---|---|
| committer | Samuel Mimram <smimram@debian.org> | 2006-11-23 14:28:36 +0000 |
| commit | b9343b970c40160fdd0329590a03fdec097de54c (patch) | |
| tree | b272880599428e1c22e577dc3eeff659fe0003fc /debian/patches/00list | |
| parent | 94594cf938e4523e60c2a750d56e5a4ab6ca5a42 (diff) | |
Skip complexity checks.debian/8.1.gamma-2
Diffstat (limited to 'debian/patches/00list')
| -rw-r--r-- | debian/patches/00list | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/debian/patches/00list b/debian/patches/00list index 5e873f10..9e577fa3 100644 --- a/debian/patches/00list +++ b/debian/patches/00list @@ -2,3 +2,4 @@ coqdoc_stdlib browser makefile system +no-complexity-test |