diff options
author | Bernhard Schommer <bernhardschommer@gmail.com> | 2018-08-01 17:31:14 +0200 |
---|---|---|
committer | Bernhard Schommer <bernhardschommer@gmail.com> | 2018-08-01 17:31:14 +0200 |
commit | a2064197c9dc5578e6f0155b8d0cc9cb3eecef90 (patch) | |
tree | f28544d73980053c7fe096110885abe7bc369622 /Makefile.extr | |
parent | 3939a1ccfdb86795e9fdf5953489ddfee238152c (diff) | |
download | compcert-a2064197c9dc5578e6f0155b8d0cc9cb3eecef90.tar.gz compcert-a2064197c9dc5578e6f0155b8d0cc9cb3eecef90.zip |
Added Pldi to instr_size.
Since Pldi generates two instructions instr_size of Pldi should
return 2.
Bug 24218
Diffstat (limited to 'Makefile.extr')
0 files changed, 0 insertions, 0 deletions