Update Changes for GPR#1525

2019-01-16 10:05:25 +01:00 · 2019-01-16 10:05:25 +01:00 · aa97ff13eb
parent 1aa856270b
commit aa97ff13eb
1 changed files with 3 additions and 0 deletions
--- a/3
+++ b/3
@ -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