Add opt-in source-line tracking for editor scroll-sync#262

dereuromark merged 1 commit into

masterphp-collective/djot-php:masterfrom

feature/source-line-trackingphp-collective/djot-php:feature/source-line-trackingCopy head branch name to clipboard