Hi, I am running F19 beta with the cinnamon desktop.

I run a few PCs which I access headlessly and I like to create terminal profile shortcuts to these and drop them into my panel for easy launch. I am having difficulty creating access to a new PC but that is my problem to solve. I set up a terminal profile but I can't change it until I access it and I obviously entered something wrong because I can't access the terminal.

What I can't work out is how do I modify or delete a profile? To create, from the Gnome terminal File->New Profile and add specific details. I can then use File->Open Terminal or File-> Open Tab to launch the terminal. Edit->Profile Preferences allows me to modify the existing terminal. But I can't see any way to File->Delete Profile. Any ideas?

Edit -> Profiles.

A box will pop up listing existing profiles. Select you one you want, then click delete.

I only get edit->Profile Preferences. No edit->Profiles option

I am wondering whether terminal v3.8.3 is a transitory version as the alt key does not work to invoke the options at the top!

I'm wondering if the GNOME team yet again decided this was an essential feature that was no longer required. Why have profiles if they can't be managed? The Profiles dialog was the only way of deleting profiles, IIRC. And removing Alt functionality? WTH? Maybe it's possible this is a bug.

I really like GNOME 3 but the team's insistence on stripping out necessary features is really pissing me off.

I'm sorry I could not be of more help.

Don't know if you ever found this.

Edit -> Preferences -> General -> Enable Mneunomics.

This will allow you to use Alt+F for File, ALt+E for Edit, etc. The only thing is the appropriate key will not be underlined on the menubar.

thanks for that goumba. Nice to know.

I must have forgot to post regarding profiles: Edit -> Preferences -> Profiles allows you to manage profiles