doc/user/permissions: update option and menu names

## What does this MR do?

This fixes `doc/user/permissions.md` documentation.

## Are there points in the code the reviewer needs to double check?

The reviewer can check that the name of the option is now **Public pipelines** and that this option is in **Project Settings > CI/CD Pipelines**.

## Why was this MR needed?

Because the previous name of the option and of the menu had not been updated in `doc/user/permissions.md` when they were changed.

## Screenshots (if relevant)

## Does this MR meet the acceptance criteria?

This is a documentation only MR, so I don't think it needs to pass all these acceptance criteria.

- [ ] [CHANGELOG](https://gitlab.com/gitlab-org/gitlab-ce/blob/master/CHANGELOG) entry added
- [ ] [Documentation created/updated](https://gitlab.com/gitlab-org/gitlab-ce/blob/master/doc/development/doc_styleguide.md)
- [ ] API support added
- Tests
  - [ ] Added for this feature/bug
  - [ ] All builds are passing
- [ ] Conform by the [merge request performance guides](http://docs.gitlab.com/ce/development/merge_request_performance_guidelines.html)
- [ ] Conform by the [style guides](https://gitlab.com/gitlab-org/gitlab-ce/blob/master/CONTRIBUTING.md#style-guides)
- [ ] Branch has no merge conflicts with `master` (if you do - rebase it please)
- [ ] [Squashed related commits together](https://git-scm.com/book/en/Git-Tools-Rewriting-History#Squashing-Commits)

## What are the relevant issue numbers?

I don't know of any issue number.

See merge request !6302