diff options
| author | Théo Zimmermann | 2019-04-30 11:42:23 +0200 |
|---|---|---|
| committer | Théo Zimmermann | 2019-05-05 19:23:27 +0200 |
| commit | 81301b55df9c52fe5503421eb9527bb04a1643e0 (patch) | |
| tree | 14cf08848ff1178e150d713c3a41386843d974b4 | |
| parent | 30d6ffdd4546d56c517bef5b31a862c5454240f0 (diff) | |
Create categories in changelog.
20 files changed, 42 insertions, 4 deletions
diff --git a/.gitattributes b/.gitattributes index 58b1a31d36..260e3f96b6 100644 --- a/.gitattributes +++ b/.gitattributes @@ -54,6 +54,7 @@ dune* whitespace=blank-at-eol,tab-in-indent .gitattributes whitespace=blank-at-eol,tab-in-indent _CoqProject whitespace=blank-at-eol,tab-in-indent Dockerfile whitespace=blank-at-eol,tab-in-indent +00000-title.rst -whitespace # tabs are allowed in Makefiles. Makefile* whitespace=blank-at-eol diff --git a/doc/changelog/00000-title.rst b/doc/changelog/00-title.rst index 628d9c8578..628d9c8578 100644 --- a/doc/changelog/00000-title.rst +++ b/doc/changelog/00-title.rst diff --git a/doc/changelog/01-kernel/00000-title.rst b/doc/changelog/01-kernel/00000-title.rst new file mode 100644 index 0000000000..f680628a05 --- /dev/null +++ b/doc/changelog/01-kernel/00000-title.rst @@ -0,0 +1,3 @@ + +**Kernel** + diff --git a/doc/changelog/02-specification-language/00000-title.rst b/doc/changelog/02-specification-language/00000-title.rst new file mode 100644 index 0000000000..99bd2c5b44 --- /dev/null +++ b/doc/changelog/02-specification-language/00000-title.rst @@ -0,0 +1,3 @@ + +**Specification language, type inference** + diff --git a/doc/changelog/03-notations/00000-title.rst b/doc/changelog/03-notations/00000-title.rst new file mode 100644 index 0000000000..abc532df11 --- /dev/null +++ b/doc/changelog/03-notations/00000-title.rst @@ -0,0 +1,3 @@ + +**Notations** + diff --git a/doc/changelog/04-tactics/00000-title.rst b/doc/changelog/04-tactics/00000-title.rst new file mode 100644 index 0000000000..3c7802d632 --- /dev/null +++ b/doc/changelog/04-tactics/00000-title.rst @@ -0,0 +1,3 @@ + +**Tactics** + diff --git a/doc/changelog/09996-hint-mode.rst b/doc/changelog/04-tactics/09996-hint-mode.rst index 06e9059b45..06e9059b45 100644 --- a/doc/changelog/09996-hint-mode.rst +++ b/doc/changelog/04-tactics/09996-hint-mode.rst diff --git a/doc/changelog/10059-change-no-check.rst b/doc/changelog/04-tactics/10059-change-no-check.rst index 987b2a8ccd..987b2a8ccd 100644 --- a/doc/changelog/10059-change-no-check.rst +++ b/doc/changelog/04-tactics/10059-change-no-check.rst diff --git a/doc/changelog/05-tactic-language/00000-title.rst b/doc/changelog/05-tactic-language/00000-title.rst new file mode 100644 index 0000000000..b34d190298 --- /dev/null +++ b/doc/changelog/05-tactic-language/00000-title.rst @@ -0,0 +1,3 @@ + +**Tactic language** + diff --git a/doc/changelog/06-ssreflect/00000-title.rst b/doc/changelog/06-ssreflect/00000-title.rst new file mode 100644 index 0000000000..2e724627ec --- /dev/null +++ b/doc/changelog/06-ssreflect/00000-title.rst @@ -0,0 +1,3 @@ + +**SSReflect** + diff --git a/doc/changelog/09995-notations.rst b/doc/changelog/06-ssreflect/09995-notations.rst index 3dfc45242d..3dfc45242d 100644 --- a/doc/changelog/09995-notations.rst +++ b/doc/changelog/06-ssreflect/09995-notations.rst diff --git a/doc/changelog/07-commands-and-options/00000-title.rst b/doc/changelog/07-commands-and-options/00000-title.rst new file mode 100644 index 0000000000..1a0272983e --- /dev/null +++ b/doc/changelog/07-commands-and-options/00000-title.rst @@ -0,0 +1,3 @@ + +**Commands and options** + diff --git a/doc/changelog/08-tools/00000-title.rst b/doc/changelog/08-tools/00000-title.rst new file mode 100644 index 0000000000..bf462744fb --- /dev/null +++ b/doc/changelog/08-tools/00000-title.rst @@ -0,0 +1,3 @@ + +**Tools** + diff --git a/doc/changelog/09-coqide/00000-title.rst b/doc/changelog/09-coqide/00000-title.rst new file mode 100644 index 0000000000..0fc27cf380 --- /dev/null +++ b/doc/changelog/09-coqide/00000-title.rst @@ -0,0 +1,3 @@ + +**CoqIDE** + diff --git a/doc/changelog/10-standard-library/00000-title.rst b/doc/changelog/10-standard-library/00000-title.rst new file mode 100644 index 0000000000..d517a0e709 --- /dev/null +++ b/doc/changelog/10-standard-library/00000-title.rst @@ -0,0 +1,3 @@ + +**Standard library** + diff --git a/doc/changelog/09984-pairusualdecidabletypefull.rst b/doc/changelog/10-standard-library/09984-pairusualdecidabletypefull.rst index 732c088f45..732c088f45 100644 --- a/doc/changelog/09984-pairusualdecidabletypefull.rst +++ b/doc/changelog/10-standard-library/09984-pairusualdecidabletypefull.rst diff --git a/doc/changelog/11-infrastructure-and-dependencies/00000-title.rst b/doc/changelog/11-infrastructure-and-dependencies/00000-title.rst new file mode 100644 index 0000000000..6b301f59d3 --- /dev/null +++ b/doc/changelog/11-infrastructure-and-dependencies/00000-title.rst @@ -0,0 +1,3 @@ + +**Infrastructure and dependencies** + diff --git a/doc/changelog/12-misc/00000-title.rst b/doc/changelog/12-misc/00000-title.rst new file mode 100644 index 0000000000..5e709e2b27 --- /dev/null +++ b/doc/changelog/12-misc/00000-title.rst @@ -0,0 +1,3 @@ + +**Miscellaneous** + diff --git a/doc/changelog/README.md b/doc/changelog/README.md index 64359e45ba..2891eb207e 100644 --- a/doc/changelog/README.md +++ b/doc/changelog/README.md @@ -14,9 +14,10 @@ entry in [`dev/doc/changes.md`](../../dev/doc/changes.md). ## How to add an entry? ## -You should create a file in this folder. The name of the file should -be `NNNNN-identifier.rst` where `NNNNN` is the number of the pull -request on five digits and `identifier` is whatever you want. +You should create a file in one of the sub-directories. The name of +the file should be `NNNNN-identifier.rst` where `NNNNN` is the number +of the pull request on five digits and `identifier` is whatever you +want. This file should use the same format as the reference manual (as it will be copied in there). You may reference the documentation you just @@ -23,7 +23,7 @@ (rule (targets unreleased.rst) (deps (source_tree changelog)) - (action (with-stdout-to %{targets} (bash "cat changelog/*.rst")))) + (action (with-stdout-to %{targets} (bash "cat changelog/00-title.rst changelog/*/*.rst")))) ; The install target still needs more work. ; (install |
