aboutsummaryrefslogtreecommitdiffhomepage
path: root/dev/tools
ModeNameSize
-rwxr-xr-xbackport-pr.sh2273logplain
-rwxr-xr-xchange-header1396logplain
-rwxr-xr-xcheck-eof-newline.sh1083logplain
-rwxr-xr-xcheck-overlays.sh279logplain
-rwxr-xr-xcheck-owners-pr.sh809logplain
-rwxr-xr-xcheck-owners.sh3891logplain
-rw-r--r--coqdev.el5981logplain
-rwxr-xr-xgithub-check-prs.py1508logplain
-rwxr-xr-xmerge-pr.sh5733logplain
-rw-r--r--objects.el3960logplain
-rwxr-xr-xpre-commit2585logplain
-rwxr-xr-xsudo-apt-get-update.sh163logplain