Revert "dash: Use pin instead of favorites"

requested review from @3v1n0-guest

@jbicha: I asked Marco to review, but it would be good if also you could have a look. Is the reasoning in the commit message in line with our IRC discussion?

Mhmhm, while I think this is fine for ubuntu session, I think we should not do this when not running the ubuntu session (i.e. with the dock by default).

So, I'm merging this as it is, but I will actually include a check to apply this only when running in the ubuntu session, as in the GNOME vanilla session it still makes sense to have the new strings.

added 6 commits

• 98e51203...0fb70b06 - 5 commits from branch gnome-team:ubuntu/master
• 338bf7bd - Revert "dash: Use pin instead of favorites"

Compare with previous version

merged

@3v1n0-guest: Thanks for merging and for improving it in next commit.

Just a thought for next release: We'd better make up our mind about what the thing with the icons is called. Ubuntu has called it "Dock" all since Ubuntu 17.10, while GNOME has called it "Dash". The label "Add to Favorites" has been neutral with respect to that, while "Pin to Dash" is not. It's desirable that we figure out a solution where the terminology in the Ubuntu session is consistent.

Yeah, I agree...

I was thinking the same as you when looking at the changes, the problem is that the dock needs to handle them and we don't want to patch even those paths, so maybe we should just use Pin everywhere?

Pin instead of Add is reasonably uncontroversial, but renaming the thing from Dock to Dash to make maintenance easier would need some further thought. "Dock" has been used everywhere — in external articles about Ubuntu, in the Appearance window, in the names of the related extensions...

Dash is such an unusual word. I'm still hopeful that one day there might be a Dock option in core GNOME.