#!/bin/sh if [ -z "$XDG_MENU_PREFIX" ] && { [ -n "`echo "$DESKTOP_SESSION" | grep "gnome"`" ] || [ "$DESKTOP_SESSION" = "cinnamon" ]; } then export XDG_MENU_PREFIX=gnome- fi