aboutsummaryrefslogtreecommitdiffhomepage
path: root/dev/tools
ModeNameSize
-rwxr-xr-xbackport-pr.sh1954logplain
-rwxr-xr-xchange-header1396logplain
-rwxr-xr-xcheck-eof-newline.sh127logplain
-rw-r--r--coqdev.el4058logplain
-rwxr-xr-xmerge-pr.sh1254logplain
-rw-r--r--objects.el3960logplain
-rwxr-xr-xshould-check-whitespace.sh224logplain