coq - The formal proof system

Age	Commit message (Collapse)	Author
2019-02-21	Merge PR #9388: merge-pr.sh: fix #9387: quick_conf doesn't work in emacs ↵	Emilio Jesus Gallego Arias
	shell buffer Reviewed-by: ejgallego
2019-02-04	Remove AppVeyor: superseded by Azure.	Théo Zimmermann

2019-01-23	merge-pr.sh: fix #9387: quick_conf doesn't work in emacs shell buffer	Gaëtan Gilbert

2019-01-22	Remove travis	Gaëtan Gilbert
	The azure OSX job replaces the first travis job, and the second always fails and so is useless.
2019-01-17	Fix merge-pr.sh when multiple review comments	Gaëtan Gilbert
	It used to output duplicate trailers.
2019-01-08	merge-pr: add reviewer info to commit message	Gaëtan Gilbert
	This produces a commit message like ~~~ Merge PR #9250: coqchk: fix check for kelim with functors Reviewed-by: ppedrot Ack-by: mattam92 ~~~
2018-11-18	merge-pr: Improve overlay check	Gaëtan Gilbert

2018-06-09	[merge script] Check if the CI that was run is outdated.	Théo Zimmermann
	[ci skip]
2018-04-11	merge script support https + typos in doc	Pierre Courtieu

2018-04-09	Merge script: adds a way for confirmation to expect a newline.	Théo Zimmermann
	This fulfils Gaetan's wish.
2018-04-09	Add sanity check in merge script: local branch is up-to-date.	Théo Zimmermann
	In case the local branch is ahead of upstream, we only print a warning because it could be that we are merging several PRs in a row.
2018-04-08	Document requirement to have git >= 2.7 to use the merge script.	Théo Zimmermann
	As reported in https://github.com/coq/coq/issues/7097#issuecomment-378632415
2018-04-08	Merge script does not warn when the remote is set to HTTPS.	Théo Zimmermann
	This should solve Emilio's problem.
2018-04-08	Merge script: use fetch URL for the remote.	Théo Zimmermann
	In case the push URL has been overriden to make it fetch-only.
2018-04-05	Improve shell scripts	zapashcanon

2018-04-03	merge-pr.sh: cache github API calls	Gaëtan Gilbert

2018-03-23	improve merge-pr script	Enrico Tassi
	The script now performs many more checks and reports errors in a more intelligible way.
2018-01-16	merge-pr.sh: use git diff --quiet	Gaëtan Gilbert

2018-01-16	Cleanup shell expansions and quoting.	Gaëtan Gilbert

2017-11-29	This script apparently uses bash-specific features.	Théo Zimmermann

2017-11-29	Fix PR merge script.	Théo Zimmermann
	Was still relying on the existence of user-configured /pr/.
2017-11-28	Add PR merge script.	Maxime Dénès