[m-dev.] diff: move the initialisation of MR_mmc_options in MR_trace_event_external()

[Erwan Jahier]

| | Fergus Henderson wrote:
| 
| [...]
| 
| | I had a more detailed look at the order of initialization, and I think
| | it should be OK to initialize MR_mmc_options in MR_trace_init_external.
| | So doing the initialization there is probably a better idea.
| | 
| 
| Here is the new diff
| 
| Estimated hours taken: 0.1
| 
| Initialise the variable MR_mmc_options in MR_trace_init_external() rather 
| than in MR_trace_event_external().
| 
| 
| only if an interactive query request is
| made; it is useless to pay the price of a call to MR_TRACE_CALL_MERCURY() for
| the other kinds of requests.
| 

Oops. Cut and paste error here. You can ignore those last 3 lines.
-- 
R1.


--------------------------------------------------------------------------
mercury-developers mailing list
Post messages to:       mercury-developers at cs.mu.oz.au
Administrative Queries: owner-mercury-developers at cs.mu.oz.au
Subscriptions:          mercury-developers-request at cs.mu.oz.au
--------------------------------------------------------------------------