diff options
Diffstat (limited to 'runtime')
| -rw-r--r-- | runtime/c/write_profiling_table.c | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/runtime/c/write_profiling_table.c b/runtime/c/write_profiling_table.c index 3c7303e4..60bae3d7 100644 --- a/runtime/c/write_profiling_table.c +++ b/runtime/c/write_profiling_table.c @@ -46,5 +46,5 @@ void _compcert_write_profiling_table(unsigned int nr_items, perror("write CompCert profiling data"); return; } - //fprintf(stderr, "no error\n"); + fprintf(stderr, "write CompCert profiling data: no error\n"); } |