diff options
| -rw-r--r-- | mk/config.mk.in | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/mk/config.mk.in b/mk/config.mk.in index bc31ba292a..10e589a934 100644 --- a/mk/config.mk.in +++ b/mk/config.mk.in @@ -1152,6 +1152,10 @@ WAY_debug_p_HC_OPTS=-optc-DDEBUG -prof WAY_debug_u_NAME=debug unregisterised WAY_debug_u_HC_OPTS=-optc-DDEBUG -unreg +# Way 'debug_t': +WAY_debug_t_NAME=debug ticky-ticky profiling +WAY_debug_t_HC_OPTS= -ticky -optc-DDEBUG + # Way 'thr_debug': WAY_thr_debug_NAME=threaded WAY_thr_debug_HC_OPTS=-optc-DTHREADED_RTS -optc-DDEBUG |