Merge pull request #1018 from jgmdev/PR/linewrapping-priority

plugin linewrapping: added priority
This commit is contained in:
Jefferson González 2022-06-03 13:28:03 -04:00 committed by GitHub
commit b70069572e
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
1 changed files with 1 additions and 1 deletions

View File

@ -1,4 +1,4 @@
-- mod-version:3
-- mod-version:3 --priority:10
local core = require "core"
local common = require "core.common"
local DocView = require "core.docview"