1 comment

Sorry, this has changed to $PROJECT_HOME/.mps/workspace.xml quite some time ago. I'll update the documentation accordingly.

0

Please sign in to leave a comment.