diff options
author | 2016-11-06 11:48:06 +0100 | |
---|---|---|
committer | 2016-11-06 11:48:06 +0100 | |
commit | bf8827788d1d8c0dc96b963d3c35985d8b3725c6 (patch) | |
tree | e9bd3245c3b5c14bbddd134863cf2af69761054a /doc | |
parent | ceaafcde70e0ba536cae03baa740563aff47f6e8 (diff) |
Hugo's comments
Diffstat (limited to 'doc')
-rw-r--r-- | doc/refman/RefMan-pre.tex | 2 |
1 files changed, 0 insertions, 2 deletions
diff --git a/doc/refman/RefMan-pre.tex b/doc/refman/RefMan-pre.tex index 944cd4848..6ba2f850e 100644 --- a/doc/refman/RefMan-pre.tex +++ b/doc/refman/RefMan-pre.tex @@ -1106,8 +1106,6 @@ over 100 contributions integrated. The main user visible changes are: Cyprien Mangin, Matthieu Sozeau and Arnaud Spiwack. \item Tactic behavior uniformization and specification, generalization of intro-patterns by Hugo Herbelin and others. -\item Update of the beautifier by Hugo Herbelin, useful for switching - between versions. \item A brand new warning system allowing to control warnings, turn them into errors or ignore them selectively by Maxime Dénès, Guillaume Melquiond and others. |