diff options
| author | Bernhard Schommer <bernhardschommer@gmail.com> | 2016-03-16 12:14:05 +0100 |
|---|---|---|
| committer | Bernhard Schommer <bernhardschommer@gmail.com> | 2016-03-16 12:14:05 +0100 |
| commit | 9d95c2ce76bffe4be06697ac99936c7703c18a07 (patch) | |
| tree | 4746470ed28516f932ae2762bfcbc434ae7f5f63 /powerpc/AsmToJSON.ml | |
| parent | 7035f06bf453bdf2f9f09fd8a392778e9ad3cd43 (diff) | |
| download | compcert-kvx-9d95c2ce76bffe4be06697ac99936c7703c18a07.tar.gz compcert-kvx-9d95c2ce76bffe4be06697ac99936c7703c18a07.zip | |
Change atom printer to use the common function.
The printer for atom constants should also use the printer
for singleton objects.
Bug 18394
Diffstat (limited to 'powerpc/AsmToJSON.ml')
| -rw-r--r-- | powerpc/AsmToJSON.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/powerpc/AsmToJSON.ml b/powerpc/AsmToJSON.ml index 48e8f766..7862aad8 100644 --- a/powerpc/AsmToJSON.ml +++ b/powerpc/AsmToJSON.ml @@ -34,7 +34,7 @@ let p_freg oc reg = let p_atom oc a = p_jstring oc (extern_atom a) -let p_atom_constant oc a = fprintf oc "{\"Atom\":%a}" p_atom a +let p_atom_constant oc a = p_jsingle_object oc "Atom" p_atom a let p_int oc i = fprintf oc "%ld" (camlint_of_coqint i) let p_int64 oc i = fprintf oc "%Ld" (camlint64_of_coqint i) |