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