aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins
diff options
context:
space:
mode:
authorGravatar Hugo Herbelin <Hugo.Herbelin@inria.fr>2015-02-01 15:11:14 +0100
committerGravatar Hugo Herbelin <Hugo.Herbelin@inria.fr>2015-02-12 17:20:35 +0100
commitbff2b36cb0e2dbd02c4f181fba545a420e847767 (patch)
treeaf281e4201f2e1cbee3aaf6c2d1d07fadbc9b4be /plugins
parent5268efdefb396267bfda0c17eb045fa2ed516b3c (diff)
Capital letter in plugins.
Diffstat (limited to 'plugins')
-rw-r--r--plugins/setoid_ring/newring.ml42
1 files changed, 1 insertions, 1 deletions
diff --git a/plugins/setoid_ring/newring.ml4 b/plugins/setoid_ring/newring.ml4
index 2f9e8509c..f040de33c 100644
--- a/plugins/setoid_ring/newring.ml4
+++ b/plugins/setoid_ring/newring.ml4
@@ -260,7 +260,7 @@ let rec dest_rel t =
(****************************************************************************)
(* Library linking *)
-let plugin_dir = "setoid_ring"
+let plugin_dir = "Setoid_ring"
let cdir = ["Coq";plugin_dir]
let plugin_modules =