GNOME Shell extension - Drop Down Terminal
https://extensions.gnome.org/extension/442/drop-down-terminal/
Drop Down Terminal はGNOME Shell 3.5.2 (正確にはgjs >= 1.33.2 and vte3 >= 0.31, gnome-shell >= 3.2 らしい)以降で動作する、ターミナル画面を表示するためのGNOME Shell 拡張機能です。Ubuntu 12.10 + GNOME Shell 3.5.92 の環境で使ってみました。
GNOME Shell のデスクトップ環境で[F12]キーを押下すると、画面の上部に半透明なターミナル画面が瞬時に表示されます。もう一度[F12]キーを押すとターミナル画面が隠れます。作者のコメントによると、キーバインドはgsettings やdconf-editor でカスタマイズできるようです。
ちょっとしたターミナル操作をする場合にとても便利です。クリップボードからのペーストは[Shift]-[Insert]が使用できます。フォーカスが合っていない場合はマウスでクリックすると良いようです。
Comment