summaryrefslogtreecommitdiff
path: root/Changes
diff options
context:
space:
mode:
authorStefan Muenzel <source@s.muenzel.net>2023-03-22 20:06:06 +0700
committerGitHub <noreply@github.com>2023-03-22 14:06:06 +0100
commit2231b5e83c504e743e3c6c18f6bf38ebaa865b1a (patch)
tree0d1452d283390458cad22c2f6ee34283b1e38352 /Changes
parent70a96837742c070f54000274c1b23d3eaf43e61d (diff)
downloadocaml-2231b5e83c504e743e3c6c18f6bf38ebaa865b1a.tar.gz
Add Misc.print_see_manual for easier printing of "see manual section X.Y.Z" (#12125)
Diffstat (limited to 'Changes')
-rw-r--r--Changes4
1 files changed, 4 insertions, 0 deletions
diff --git a/Changes b/Changes
index 8b181edc84..d5c62b1b20 100644
--- a/Changes
+++ b/Changes
@@ -552,6 +552,10 @@ Working version
cu_required_globals field of compilation unit descriptors.
(Sébastien Hinderer, review by Vincent Laviron)
+- #12125: Add Misc.print_see_manual and modify [@manual_ref] to accept
+ lists for simpler printing of manual references
+ (Stefan Muenzel, review by Florian Angeletti)
+
### Build system:
- #11590: Allow installing to a destination path containing spaces.