aboutsummaryrefslogtreecommitdiff
path: root/dev/tools
AgeCommit message (Expand)Author
2020-07-15Compatibility of make-change-log with MacOS X whose "sed" does not support "\+".Hugo Herbelin
2020-05-25dev/tools/make-changelog.sh now asks about fixed bugsJason Gross
2020-05-23[dev/tools] Fix #12314: do not die silently if branch has no remote.Théo Zimmermann
2020-05-22[backport-pr] Select correct remote of the master branch.Théo Zimmermann
2020-05-20[merge-pr] Use a simpler method to get all pagesJason Gross
2020-05-20[merge-pr.sh] Follow next links insteadJason Gross
2020-05-20Use pagination in fetching the number of reviewsJason Gross
2020-05-15Merge PR #11979: Add a rudimentary script to generate release changelog.Emilio Jesus Gallego Arias
2020-04-09[pre-commit] Check ocamlformat version and silence ocamlformat.Théo Zimmermann
2020-04-03Support when release branch is checked out in a worktree.Théo Zimmermann
2020-04-03Add a rudimentary script to generate release changelog.Théo Zimmermann
2020-04-01Merge PR #11873: python3 script does not need to import from the futureEmilio Jesus Gallego Arias
2020-03-30Fix commit hook when there are no changes (eg amend message)Gaëtan Gilbert
2020-03-24Run ocamlformat on modified ml / mli files in pre-commit hook.Théo Zimmermann
2020-03-20python3 script does not need to import from the futureRalf Treinen
2020-03-18Also show unchanged headers.Théo Zimmermann
2020-02-24Remove hard to read blue color in merge-prGaëtan Gilbert
2020-02-21[merge-script] Improve warning in case of batch merging.Théo Zimmermann
2020-01-19Merge PR #11214: Add a script to pin CI developments.Gaëtan Gilbert
2020-01-07[merge script] Never bypass outdated branch sanity check.Théo Zimmermann
2019-12-02Remove deprecated compat modifier of Notation / Infix commands.Théo Zimmermann
2019-12-02Add a script to pin CI developments.Pierre-Marie Pédrot
2019-11-28Update README and make-changelog tool following introduction of changelog types.Théo Zimmermann
2019-11-25Error fatally if update-compat.py gets no flagJason Gross
2019-11-12Printing name of change log file in changelog script.Hugo Herbelin
2019-10-30Make changelog script aware of trailing slashes.Arthur Azevedo de Amorim
2019-10-11Simple script to prefill a changelog entryGaëtan Gilbert
2019-07-09merge-pr.sh: filter reviews to remove the PR authorGaëtan Gilbert
2019-07-06[python] Remove use of generic python shebang, update CIEmilio Jesus Gallego Arias
2019-06-17Adapt change-header script to handle shebangs in addition to Emacs comments.Théo Zimmermann
2019-06-17Update change-header script to support updating more than just files with ml-...Théo Zimmermann
2019-06-12Merge PR #10180: `deprecated` attribute support for notations and syntactic d...Théo Zimmermann
2019-06-06`deprecated` attribute support for notations and syntactic definitionsMaxime Dénès
2019-05-24Update coqdev-setup-proofgeneral for duneGaëtan Gilbert
2019-05-22Better dune ocamldebug integrationGaëtan Gilbert
2019-03-26Improve the backport script.Guillaume Melquiond
2019-03-01Update coqdev.el to use -topfileGaëtan Gilbert
2019-02-21Merge PR #9618: [dev/tools/create_overlays] remove trailing whitespaceEmilio Jesus Gallego Arias
2019-02-21remove meta trailing whitespaceEnrico Tassi
2019-02-21Merge PR #9388: merge-pr.sh: fix #9387: quick_conf doesn't work in emacs shel...Emilio Jesus Gallego Arias
2019-02-04Remove AppVeyor: superseded by Azure.Théo Zimmermann
2019-01-29Update update-compat.py scriptJason Gross
2019-01-29Merge PR #9383: Remove travisVincent Laporte
2019-01-24Update update-compat.py and release-process.mdJason Gross
2019-01-24Update update-compat.py scriptJason Gross
2019-01-23merge-pr.sh: fix #9387: quick_conf doesn't work in emacs shell bufferGaëtan Gilbert
2019-01-22Remove travisGaëtan Gilbert
2019-01-17Fix merge-pr.sh when multiple review commentsGaëtan Gilbert
2019-01-08merge-pr: add reviewer info to commit messageGaëtan Gilbert
2018-11-23Merge PR #9055: [dev] fix create_overlay wrt branch names containing /Emilio Jesus Gallego Arias
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 18:42:50 +0000