diff --git a/branches/newMo/src/explorer/moTSExplorer.h b/branches/newMo/src/explorer/moTSExplorer.h index adec8cc25..b00cdbd2c 100644 --- a/branches/newMo/src/explorer/moTSExplorer.h +++ b/branches/newMo/src/explorer/moTSExplorer.h @@ -121,7 +121,7 @@ public: /** - * + * terminate : NOTHING TO DO */ virtual void terminate(EOT & solution) {