aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorThéo Zimmermann2019-04-30 11:42:23 +0200
committerThéo Zimmermann2019-05-05 19:23:27 +0200
commit81301b55df9c52fe5503421eb9527bb04a1643e0 (patch)
tree14cf08848ff1178e150d713c3a41386843d974b4
parent30d6ffdd4546d56c517bef5b31a862c5454240f0 (diff)
Create categories in changelog.
-rw-r--r--.gitattributes1
-rw-r--r--doc/changelog/00-title.rst (renamed from doc/changelog/00000-title.rst)0
-rw-r--r--doc/changelog/01-kernel/00000-title.rst3
-rw-r--r--doc/changelog/02-specification-language/00000-title.rst3
-rw-r--r--doc/changelog/03-notations/00000-title.rst3
-rw-r--r--doc/changelog/04-tactics/00000-title.rst3
-rw-r--r--doc/changelog/04-tactics/09996-hint-mode.rst (renamed from doc/changelog/09996-hint-mode.rst)0
-rw-r--r--doc/changelog/04-tactics/10059-change-no-check.rst (renamed from doc/changelog/10059-change-no-check.rst)0
-rw-r--r--doc/changelog/05-tactic-language/00000-title.rst3
-rw-r--r--doc/changelog/06-ssreflect/00000-title.rst3
-rw-r--r--doc/changelog/06-ssreflect/09995-notations.rst (renamed from doc/changelog/09995-notations.rst)0
-rw-r--r--doc/changelog/07-commands-and-options/00000-title.rst3
-rw-r--r--doc/changelog/08-tools/00000-title.rst3
-rw-r--r--doc/changelog/09-coqide/00000-title.rst3
-rw-r--r--doc/changelog/10-standard-library/00000-title.rst3
-rw-r--r--doc/changelog/10-standard-library/09984-pairusualdecidabletypefull.rst (renamed from doc/changelog/09984-pairusualdecidabletypefull.rst)0
-rw-r--r--doc/changelog/11-infrastructure-and-dependencies/00000-title.rst3
-rw-r--r--doc/changelog/12-misc/00000-title.rst3
-rw-r--r--doc/changelog/README.md7
-rw-r--r--doc/dune2
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
diff --git a/doc/dune b/doc/dune
index 06f78013aa..3a8efbb36d 100644
--- a/doc/dune
+++ b/doc/dune
@@ -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