summaryrefslogtreecommitdiff
path: root/stdlib/listLabels.mli
diff options
context:
space:
mode:
authorJohn Whitington <john@coherentgraphics.co.uk>2020-07-08 12:52:57 +0100
committerJohn Whitington <john@coherentgraphics.co.uk>2020-07-08 12:52:57 +0100
commitf410787b8173f7b069837a78eca6b13ed85fc41d (patch)
treef04f521913d97568b460e1b830cbc9251873cde2 /stdlib/listLabels.mli
parentdea23a56c565046af4446a09e14d83c6cb3ea44b (diff)
downloadocaml-f410787b8173f7b069837a78eca6b13ed85fc41d.tar.gz
Better warning for developers
Diffstat (limited to 'stdlib/listLabels.mli')
-rw-r--r--stdlib/listLabels.mli8
1 files changed, 6 insertions, 2 deletions
diff --git a/stdlib/listLabels.mli b/stdlib/listLabels.mli
index 4563bf8517..df7e3ee404 100644
--- a/stdlib/listLabels.mli
+++ b/stdlib/listLabels.mli
@@ -13,8 +13,12 @@
(* *)
(**************************************************************************)
-(* NOTE: When updating listLabels.mli, run tools/unlabel to generate
- list.mli
+(* NOTE:
+ If this file is listLabels.mli, run tools/unlabel after editing it to
+ generate list.mli.
+
+ If this file is list.mli, do not edit it directly -- edit
+ listLabels.mli instead.
*)
(** List operations.