diff options
author | Robert Alessi <alessi@robertalessi.net> | 2018-10-01 14:34:53 +0200 |
---|---|---|
committer | Robert Alessi <alessi@robertalessi.net> | 2018-10-01 14:34:53 +0200 |
commit | 645fb1f4ce14786b70f2d9a3446b8fa407b4ea0f (patch) | |
tree | 5287f94c09a5016707d3acf338ffffcba70da530 | |
parent | 1d44a53c55314c698d74fa3fb8403d6ca7f81029 (diff) | |
parent | 71471d41f59ab197bd5004ab5f177e4d853da84e (diff) | |
download | arabluatex-645fb1f4ce14786b70f2d9a3446b8fa407b4ea0f.tar.gz |
Merge branch 'master' of git.robertalessi.net:git/arabluatex
-rw-r--r-- | arabluatex.lua | 7 |
1 files changed, 7 insertions, 0 deletions
diff --git a/arabluatex.lua b/arabluatex.lua index ab92174..34f59e9 100644 --- a/arabluatex.lua +++ b/arabluatex.lua | |||
@@ -832,11 +832,18 @@ function al_closestream() | |||
832 | end) | 832 | end) |
833 | if string.find(t, "\\begin%s?{document}.-\\arb%s?[%[%{]") or | 833 | if string.find(t, "\\begin%s?{document}.-\\arb%s?[%[%{]") or |
834 | string.find(t, "\\begin%s?{document}.-\\[Uu]c%s?%b{}") | 834 | string.find(t, "\\begin%s?{document}.-\\[Uu]c%s?%b{}") |
835 | <<<<<<< HEAD | ||
835 | then | 836 | then |
836 | tex.print([[\unexpanded{\PackageWarningNoLine{arabluatex}{ | 837 | tex.print([[\unexpanded{\PackageWarningNoLine{arabluatex}{ |
837 | There are still 'arabtex' strings to be converted. | 838 | There are still 'arabtex' strings to be converted. |
838 | Please open ]] .. tex.jobname .. utffilesuffix .. ".tex" .. | 839 | Please open ]] .. tex.jobname .. utffilesuffix .. ".tex" .. |
839 | [[ and compile it one more time}}]]) | 840 | [[ and compile it one more time}}]]) |
841 | ======= | ||
842 | then | ||
843 | tex.print([[\unexpanded{\PackageWarningNoLine{arabluatex}{There are still 'arabtex' strings | ||
844 | to be converted. Please open ]] .. tex.jobname .. utffilesuffix .. ".tex" .. | ||
845 | [[ and compile it one more time}}]]) | ||
846 | >>>>>>> 71471d41f59ab197bd5004ab5f177e4d853da84e | ||
840 | else end | 847 | else end |
841 | t = t.."\n\\end{document}" | 848 | t = t.."\n\\end{document}" |
842 | io.write(t) | 849 | io.write(t) |