aboutsummaryrefslogtreecommitdiffstats
path: root/exportclight
diff options
context:
space:
mode:
Diffstat (limited to 'exportclight')
-rw-r--r--exportclight/ExportClight.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/exportclight/ExportClight.ml b/exportclight/ExportClight.ml
index 87956b58..96947545 100644
--- a/exportclight/ExportClight.ml
+++ b/exportclight/ExportClight.ml
@@ -81,7 +81,7 @@ let define_idents p =
string_of_atom
(fun (id, name) ->
try
- if id = pos_of_string name then
+ if !use_canonical_atoms && id = pos_of_string name then
fprintf p "Definition _%s : ident := $\"%s\".@ "
(sanitize name) name
else