From d00472c59d15259b486868c5ccdb50b6e602a548 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Thu, 6 Dec 2018 04:44:27 +0100
Subject: [doc] Enable Warning 50 [incorrect doc comment] and fix comments.

This is a pre-requisite to use automated formatting tools such as
`ocamlformat`, also, there were quite a few places where the comments
had basically no effect, thus it was confusing for the developer.

p.s: Reading some comments was a lot of fun :)
---
 printing/proof_diffs.mli | 1 +
 1 file changed, 1 insertion(+)

(limited to 'printing/proof_diffs.mli')

diff --git a/printing/proof_diffs.mli b/printing/proof_diffs.mli
index ce9ee5ae6f..1ebde3d572 100644
--- a/printing/proof_diffs.mli
+++ b/printing/proof_diffs.mli
@@ -12,6 +12,7 @@
 
 (** Controls whether to show diffs.  Takes values "on", "off", "removed" *)
 val write_diffs_option : string -> unit
+
 (** Returns true if the diffs option is "on" or "removed" *)
 val show_diffs : unit -> bool
 
-- 
cgit v1.2.3