[mercury-users] Controlling the depth of term printing in 'mdb'

[Nicholas Nethercote]

Hi,

I'm using mdb.  I want to change the depth of term printing when printing 
things with 'print'.  Section 7.9.4 of the user's manual says, under the 
docs for 'print':

   Various settings which affect the way that terms are printed out
   (including e.g. the maximum term depth) can be set using the set command.

but I can't find docs for the 'set' command and the debugger doesn't seem to 
think it exists.

How do I change this?

Thanks.

Nick
--------------------------------------------------------------------------
mercury-users mailing list
Post messages to:       mercury-users at csse.unimelb.edu.au
Administrative Queries: owner-mercury-users at csse.unimelb.edu.au
Subscriptions:          mercury-users-request at csse.unimelb.edu.au
--------------------------------------------------------------------------