Documented that ContextObj::destroy() only restores back to context level 0.
authorClark Barrett <barrett@cs.nyu.edu>
Tue, 23 Mar 2010 21:30:27 +0000 (21:30 +0000)
committerClark Barrett <barrett@cs.nyu.edu>
Tue, 23 Mar 2010 21:30:27 +0000 (21:30 +0000)
commit876993722316c92f6d24525e22c89c215ac90521
treee635a9f8c1d7510251c1a76154add82e77c0c61d
parente11bce2790fa9e517e08ae5d3c477da651db3630
Documented that ContextObj::destroy() only restores back to context level 0.
If there is more cleanup to do, it has to be done by the destructor.
src/context/context.h