Setting RTS options for snippets also affects server

fpco / ide-backend

ide-backend drives the GHC API to build, query, and run your code

120 stars 17 forks source link

Setting RTS options for snippets also affects server #266

Open edsko opened 9 years ago

edsko commented 9 years ago

When changing RTS options we restart the main server with the new RTS options, which then, when forked, also apply to snippets. It would be nicer if we could somehow change this so that RTS options affect the execution of snippets but not of the server itself. This is tricky though.