index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
dev
/
tools
Commit message (
Expand
)
Author
Age
*
Merge script: adds a way for confirmation to expect a newline.
Théo Zimmermann
2018-04-09
*
Add sanity check in merge script: local branch is up-to-date.
Théo Zimmermann
2018-04-09
*
Document requirement to have git >= 2.7 to use the merge script.
Théo Zimmermann
2018-04-08
*
Merge script does not warn when the remote is set to HTTPS.
Théo Zimmermann
2018-04-08
*
Merge script: use fetch URL for the remote.
Théo Zimmermann
2018-04-08
*
Improve shell scripts
zapashcanon
2018-04-05
*
merge-pr.sh: cache github API calls
Gaëtan Gilbert
2018-04-03
*
pre-commit: verify user overlay extensions (must be .sh).
Gaëtan Gilbert
2018-03-31
*
improve merge-pr script
Enrico Tassi
2018-03-23
*
Merge PR #6803: coqdev.el: add space at the end of compile-command
Maxime Dénès
2018-02-24
|
\
*
\
Merge PR #6283: A pre-commit hook to magically fix whitespace issues.
Maxime Dénès
2018-02-21
|
\
\
|
|
*
coqdev.el: add space at the end of compile-command
Gaëtan Gilbert
2018-02-21
|
|
/
|
/
|
*
|
Merge PR #6556: Remove dir-locals and ship suggested helper hooks instead.
Maxime Dénès
2018-02-19
|
\
\
|
*
|
coqdev.el: wait for 'compile to touch compilation-error-regexp-alist
Gaëtan Gilbert
2018-02-13
|
*
|
coqdev.el: fix "compilate"-command typo
Gaëtan Gilbert
2018-02-13
|
*
|
coqdev.el: shell-quote-argument the directory for make -C
Gaëtan Gilbert
2018-02-13
|
*
|
coqdev.el: stop using when-let for emacs<25 compatibility.
Gaëtan Gilbert
2018-02-13
*
|
|
Merge PR #6565: [Backport script] Check .mli files are not changed.
Maxime Dénès
2018-02-12
|
\
\
\
|
|
*
|
Merge anomaly-traces-parser.el into coqdev.el.
Gaëtan Gilbert
2018-02-11
|
|
*
|
coqdev.el: add installation instructions.
Gaëtan Gilbert
2018-02-11
|
|
|
*
pre-commit: nicer messages
Gaëtan Gilbert
2018-02-08
|
|
|
*
pre-commit: fail gracefully if fixing whitespace removes all changes
Gaëtan Gilbert
2018-02-08
|
|
|
*
pre-commit: add files after fixing ending newlines.
Gaëtan Gilbert
2018-02-08
|
|
|
*
Have the pre-commit hook also fix end-of-file nl
Jason Gross
2018-02-08
|
|
|
*
Auto-create .git/hooks/pre-commit on ./configure
Jason Gross
2018-02-08
|
|
|
*
pre-commit hook: fix whitespace error detection
Gaëtan Gilbert
2018-02-08
|
|
|
*
A pre-commit hook to magically fix whitespace issues.
Gaëtan Gilbert
2018-02-08
*
|
|
|
Use travis_retry on apt-get update
Jason Gross
2018-01-23
|
|
_
|
/
|
/
|
|
*
|
|
Merge PR #6568: Cleanup scripts
Maxime Dénès
2018-01-23
|
\
\
\
|
*
|
|
merge-pr.sh: use git diff --quiet
Gaëtan Gilbert
2018-01-16
|
*
|
|
Cleanup shell expansions and quoting.
Gaëtan Gilbert
2018-01-16
|
*
|
|
Simplify logic and streamline lint-repository.sh
Gaëtan Gilbert
2018-01-16
*
|
|
|
Merge PR #6519: Python script checking missing/unnecessary [needs: rebase] label
Maxime Dénès
2018-01-10
|
\
\
\
\
|
|
|
*
|
[Backport script] Check .mli files are not changed.
Théo Zimmermann
2018-01-09
|
|
_
|
/
/
|
/
|
|
|
|
*
|
|
github-check-prs.py: print PR URLs when needed.
Gaëtan Gilbert
2018-01-08
|
*
|
|
github-check-prs.py: Strip spaces from token from command line
Gaëtan Gilbert
2018-01-08
|
*
|
|
github-check-prs.py: command line option to get token from a file
Gaëtan Gilbert
2018-01-08
|
|
|
*
Remove dir-locals and ship suggested helper hooks instead.
Gaëtan Gilbert
2018-01-06
|
|
|
/
|
*
|
Expound on dependencies for github-check-prs.py
Gaëtan Gilbert
2017-12-30
|
*
|
Python script checking missing/unnecessary [needs: rebase] label
Gaëtan Gilbert
2017-12-30
|
|
/
*
/
Update backport script for more control.
Théo Zimmermann
2017-12-24
|
/
*
Fix usage comment.
Théo Zimmermann
2017-11-29
*
This script apparently uses bash-specific features.
Théo Zimmermann
2017-11-29
*
Fix PR merge script.
Théo Zimmermann
2017-11-29
*
Add PR backport script.
Théo Zimmermann
2017-11-28
*
Add PR merge script.
Maxime Dénès
2017-11-28
*
Linter: do not lint untracked files.
Gaëtan Gilbert
2017-11-23
*
Disable whitespace linter for .out files.
Gaëtan Gilbert
2017-11-20
*
Linter: check that files end with newlines.
Gaëtan Gilbert
2017-10-25
*
Remove unused Makefiles in dev/tools/
Gaëtan Gilbert
2017-08-01
[next]