You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
Currently, GobPie assumes that gobpie.json is located at the root of the workspace where the IDE has been opened.
This could be relaxed to allow gobpie.json file to be located also in some subdirectory of the open workspace, GobPie just search the workspace for these files. Any paths and commands in gobpie.json should then be executed relative to it.
This could also allow multiple gobpie.json files to coexist in different subdirectories. Each one could correspond to an independent Goblint server, but the messages would be shown together in the single IDE instance.
The text was updated successfully, but these errors were encountered:
Actually, GobPie shouldn't eagerly start a server for each gobpie.json it finds on startup because it could have very undesired effects if there are many (e.g. our bench repo). A more reasonable alternative is the following:
If gobpie.json exists in project root, use it automatically.
For other gobpie.jsons don't use them automatically, but only after the user has opened the conf file once.
Currently, GobPie assumes that
gobpie.json
is located at the root of the workspace where the IDE has been opened.This could be relaxed to allow
gobpie.json
file to be located also in some subdirectory of the open workspace, GobPie just search the workspace for these files. Any paths and commands ingobpie.json
should then be executed relative to it.This could also allow multiple
gobpie.json
files to coexist in different subdirectories. Each one could correspond to an independent Goblint server, but the messages would be shown together in the single IDE instance.The text was updated successfully, but these errors were encountered: