Ubuntu GNOME 17.04でGPasteのバグっぽいものを修正して日本語化してみた
GPasteというGNOME環境用のクリップボードマネージャーがある。
Ubuntu 17.04と17.10のGNOME Shellで試用してみたのだが、17.10だとどうも拡張機能がフリーズするバグがあるっぽいというか、17.04でもCPUを使いまくるバグっぽい挙動が見られたので修正して、ついでに日本語化してみた。
※このバグは既に修正済です。
端末で、
sudo add-apt-repository ppa:sicklylife/ppa sudo apt update sudo apt install gnome-shell-extensions-gpaste
と実行するとインストールできる。拡張機能を有効にするには一旦ログアウトするかGNOME Shellの再起動が必要かもしれない。
ちなみに修正部分は以下の通り。
--- a/src/gnome-shell/pageSwitcher.js +++ b/src/gnome-shell/pageSwitcher.js @@ -42,7 +42,26 @@ }, updateForSize: function(size) { - const pages = Math.min((size === 0) ? 0 : Math.floor(size / this._maxDisplayedSize + 1), MAX_PAGES); +/* const pages = Math.min((size === 0) ? 0 : Math.floor(size / this._maxDisplayedSize + 1), MAX_PAGES);*/ + + var pagest; + + if (size === 0) { + pagest = 0; + } + else { + pagest = Math.floor(size / this._maxDisplayedSize); + + if ((size % this._maxDisplayedSize) > 0) { + pagest++; + } + + if (pagest > MAX_PAGES) { + pagest = MAX_PAGES; + } + } + + const pages = pagest; for (let i = this._pages.length; i < pages; ++i) { this._addPage(); @@ -87,9 +106,15 @@ setActive: function(page) { if (page !== 0 && page !== (this._active + 1) && page <= this._pages.length) { if (this._active !== -1) { - this._pages[this._active].setActive(false); +/* this._pages[this._active].setActive(false);*/ + this._pages[0].setActive(false); } this._active = page - 1; + + for (let i = 0; i < this._pages.length; ++i) { + this._pages[i].setActive(false); + } + this._pages[this._active].setActive(true); } },