diff options
Diffstat (limited to 'mk/ways.mk')
-rw-r--r-- | mk/ways.mk | 8 |
1 files changed, 0 insertions, 8 deletions
diff --git a/mk/ways.mk b/mk/ways.mk index deba1d5df8..c2dcf072fb 100644 --- a/mk/ways.mk +++ b/mk/ways.mk @@ -40,10 +40,6 @@ WAY_v_HC_OPTS= WAY_p_NAME=profiling WAY_p_HC_OPTS= -prof -# Way 't': -WAY_t_NAME=ticky-ticky profiling -WAY_t_HC_OPTS= -ticky - # Way 'l': WAY_l_NAME=event logging WAY_l_HC_OPTS= -eventlog @@ -80,10 +76,6 @@ WAY_debug_HC_OPTS=-optc-DDEBUG WAY_debug_p_NAME=debug profiled WAY_debug_p_HC_OPTS=-optc-DDEBUG -prof -# 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 |