aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/extraction
diff options
context:
space:
mode:
authorGravatar Paul Steckler <steck@stecksoft.com>2017-12-06 11:29:03 -0500
committerGravatar Paul Steckler <steck@stecksoft.com>2017-12-06 11:29:03 -0500
commit1ed79649c0435336c98a1d8b89e1ccc36b8107cc (patch)
tree2c61d0eeb94f4239c5c3af0c0cb4fe20c5e1eaf9 /plugins/extraction
parent600c1ee611a0442fd6794248327a72c53c3d4cb6 (diff)
issue deprecation warning for "Ocaml"
Diffstat (limited to 'plugins/extraction')
-rw-r--r--plugins/extraction/g_extraction.ml47
1 files changed, 6 insertions, 1 deletions
diff --git a/plugins/extraction/g_extraction.ml4 b/plugins/extraction/g_extraction.ml4
index 7cebf5d70..24c70bccf 100644
--- a/plugins/extraction/g_extraction.ml4
+++ b/plugins/extraction/g_extraction.ml4
@@ -47,9 +47,14 @@ let pr_language = function
| Scheme -> str "Scheme"
| JSON -> str "JSON"
+let warn_deprecated_ocaml_spelling =
+ CWarnings.create ~name:"deprecated-ocaml-spelling" ~category:"deprecated"
+ (fun () ->
+ strbrk ("The spelling \"OCaml\" should be used instead of \"Ocaml\"."))
+
VERNAC ARGUMENT EXTEND language
PRINTED BY pr_language
-| [ "Ocaml" ] -> [ Ocaml ] (* deprecated *)
+| [ "Ocaml" ] -> [ let _ = warn_deprecated_ocaml_spelling () in Ocaml ]
| [ "OCaml" ] -> [ Ocaml ]
| [ "Haskell" ] -> [ Haskell ]
| [ "Scheme" ] -> [ Scheme ]