1
0
mirror of https://git.FreeBSD.org/ports.git synced 2025-02-07 11:49:40 +00:00
Alexander Vereeken a7c419f27a deskutils/gnome-shell-extension-dashtopanel: add new port
This extension moves the dash into the gnome main panel.

https://github.com/home-sweet-gnome/dash-to-panel

PR:		243771
2021-05-01 05:57:33 +00:00

14 lines
370 B
Plaintext

[
{
message: <<EOM
This gnome-shell extension won't be usable until the gnome-shell
gets restarted. To do so, running the shell, press ALT+F2 and
type 'r'. That will restart the shell.
To enable or configure an extension, after restarting the shell, you
have to open a new gnome-tweak-tool instance. The new extension
should appear in the extensions section.
EOM
}
]