mirror of
https://gitflic.ru/project/openide/openide.git
synced 2025-12-15 02:59:33 +07:00
Otherwise, it cancels hyperlinks highlighter running in background, because of changed `document.getModificationStamp()`. Merge-request: IJ-MR-134015 Merged-by: Sergey Simonchik <sergey.simonchik@jetbrains.com> GitOrigin-RevId: 7a097bb634aa14875f1423304e8b023d58cd791a