-
Bug
-
Resolution: Done
-
Major
-
4.2.0.Beta1
-
None
In the past, one could change if a server is local or remote in the server editor.
Now that it's no longer possible to change the profile (as it's now called) after the server is created, it is displayed as a disabled drop down menu. Since it will never be enabled, it shouldn't probably be a drop down menu at all. Also, currently this drop down menu does not have any title.
So instead of that, I suggest just printing something like this:
Profile: <profile_name>