Merge branch 'master' into pr-hide-review-panel

This commit is contained in:
Paulo Reis 2017-05-26 09:39:29 +01:00
commit 7fbf6d97bd

View file

@ -341,7 +341,8 @@ define [
response = getChkTex()
# display the combined result
response.finally annotateFiles
if response?
response.finally annotateFiles
getRootDocOverride_id = () ->
doc = ide.editorManager.getCurrentDocValue()