fix setUseWorker()
This commit is contained in:
parent
f275f4ade4
commit
ebe4117945
2 changed files with 3 additions and 0 deletions
|
|
@ -356,6 +356,8 @@ var EditSession = function(text, mode) {
|
||||||
this.$worker.terminate();
|
this.$worker.terminate();
|
||||||
this.$worker = null;
|
this.$worker = null;
|
||||||
}
|
}
|
||||||
|
|
||||||
|
this.$useWorker = useWorker;
|
||||||
};
|
};
|
||||||
|
|
||||||
this.getUseWorker = function() {
|
this.getUseWorker = function() {
|
||||||
|
|
|
||||||
|
|
@ -21,6 +21,7 @@
|
||||||
*
|
*
|
||||||
* Contributor(s):
|
* Contributor(s):
|
||||||
* Fabian Jakobs <fabian AT ajax DOT org>
|
* Fabian Jakobs <fabian AT ajax DOT org>
|
||||||
|
* Mihai Sucan <mihai DOT sucan AT gmail DOT com>
|
||||||
*
|
*
|
||||||
* Alternatively, the contents of this file may be used under the terms of
|
* Alternatively, the contents of this file may be used under the terms of
|
||||||
* either the GNU General Public License Version 2 or later (the "GPL"), or
|
* either the GNU General Public License Version 2 or later (the "GPL"), or
|
||||||
|
|
|
||||||
Loading…
Add table
Add a link
Reference in a new issue