aboutsummaryrefslogtreecommitdiffhomepage
path: root/dev/tools
ModeNameSize
-rwxr-xr-xbackport-pr.sh2263logplain
-rwxr-xr-xchange-header1396logplain
-rwxr-xr-xcheck-eof-newline.sh334logplain
-rw-r--r--coqdev.el4100logplain
-rwxr-xr-xgithub-check-prs.py1508logplain
-rwxr-xr-xmerge-pr.sh1283logplain
-rw-r--r--objects.el3960logplain
-rwxr-xr-xsudo-apt-get-update.sh163logplain