Attention une mise à jour du serveur va être effectuée le lundi 17 mai entre 13h et 13h30. Cette mise à jour va générer une interruption du service de quelques minutes.

Commit 1e65a970 authored by POTTIER Francois's avatar POTTIER Francois

Remove an overfull hbox.

parent ea3efd8e
......@@ -2236,7 +2236,7 @@ type 'a mylist = 'a list =
[@@deriving visitors { variety = "map" }]
If desired, instead of \oc|[@name]|, one can use
\oc|[]| or \oc|[]|.
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment