diff options
| author | Thomas Bauereiss | 2018-02-16 20:01:51 +0000 |
|---|---|---|
| committer | Thomas Bauereiss | 2018-02-16 20:01:51 +0000 |
| commit | 18767e96381dc5fdd5a88fc18a355b5f67433021 (patch) | |
| tree | cc2c721a099961845f0a7182ca32b85bb0f16235 /src/reporting_basic.ml | |
| parent | 8403ad68b451f9d41baa52087af5fd7acef6bc58 (diff) | |
Don't generate undefined functions for generated register types
Diffstat (limited to 'src/reporting_basic.ml')
0 files changed, 0 insertions, 0 deletions