From aa97ff13eb2169effd6d3b70fef07ed7877a9380 Mon Sep 17 00:00:00 2001 From: Richard Bonichon Date: Wed, 16 Jan 2019 10:05:25 +0100 Subject: [PATCH] Update Changes for GPR#1525 --- Changes | 3 +++ 1 file changed, 3 insertions(+) diff --git a/Changes b/Changes index 831448094..918d692c0 100644 --- a/Changes +++ b/Changes @@ -190,6 +190,9 @@ Working version - GPR#2185: Add `List.filter_map` (Thomas Refis, review by Alain Frisch and Gabriel Scherer) +- GPR#1525: Make function set_max_indent respect documentation + (Pierre Weis, Richard Bonichon, review by Florian Angeletti) + ### Other libraries: - GPR#1061: Add ?follow parameter to Unix.link. This allows hardlinking