aboutsummaryrefslogtreecommitdiff
path: root/dev
diff options
context:
space:
mode:
Diffstat (limited to 'dev')
-rw-r--r--dev/vm_printers.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/dev/vm_printers.ml b/dev/vm_printers.ml
index 47cfeb98d7..ea126e2756 100644
--- a/dev/vm_printers.ml
+++ b/dev/vm_printers.ml
@@ -10,7 +10,7 @@ let ppripos (ri,pos) =
| Reloc_annot a ->
let sp,i = a.ci.ci_ind in
print_string
- ("annot : MutInd("^(MutInd.to_string sp)^","^(string_of_int i)^")\n")
+ ("annot : MutInd("^(MutInd.to_string sp)^","^(string_of_int i)^")\n")
| Reloc_const _ ->
print_string "structured constant\n"
| Reloc_getglobal kn ->