summaryrefslogtreecommitdiff
path: root/debian
ModeNameSize
-rw-r--r--.gitignore116logplain
-rw-r--r--ccomp.16810logplain
-rw-r--r--changelog140logplain
-rw-r--r--compat2logplain
-rw-r--r--compcert.manpages14logplain
-rw-r--r--control931logplain
-rw-r--r--copyright17204logplain
-rw-r--r--docs7logplain
-rw-r--r--gbp.conf30logplain
-rwxr-xr-xinstall116logplain
d---------patches83logplain
-rwxr-xr-xrules939logplain
d---------source34logplain
-rw-r--r--watch79logplain