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 the editor only supports changes to the entire document.
However, while programming/specifying you often only want the changes in a part of the file and not the entire file. (cf. TextWrangler e.g.)
Please consider adding the "selected text only" option.
The text was updated successfully, but these errors were encountered:
This could be a useful option, but it is not an urgent problem to be resolved for the next release.
Therefore, I postpone the request to be dealt with at a later moment.
Issue migrated from trac ticket # 1334
component: mcrl2xi | priority: minor | keywords: find, replace, editor
2015-10-01 12:04:27: Gert Veltink gert.veltink@hs-emden-leer.de created the issue
Currently the editor only supports changes to the entire document.
However, while programming/specifying you often only want the changes in a part of the file and not the entire file. (cf. TextWrangler e.g.)
Please consider adding the "selected text only" option.
The text was updated successfully, but these errors were encountered: