Skip to content
This repository was archived by the owner on Feb 15, 2022. It is now read-only.

Change 'Industry' to 'Principles' #339

Closed
ILeandersson opened this issue May 12, 2021 · 1 comment · Fixed by #376
Closed

Change 'Industry' to 'Principles' #339

ILeandersson opened this issue May 12, 2021 · 1 comment · Fixed by #376
Labels
Design-Implementation Request to implement a design suggestion good first issue Good for newcomers

Comments

@ILeandersson
Copy link

ILeandersson commented May 12, 2021 •
edited by agarwal
Loading

Change in navbar, footer, and and search for any other occurrences.

Screenshot 2021-05-12 at 14 35 08

Screenshot 2021-05-12 at 14 53 49
@ILeandersson ILeandersson added the Design-Implementation Request to implement a design suggestion label May 12, 2021
@ghost ghost added the good first issue Good for newcomers label May 12, 2021
@agarwal agarwal changed the title Navbar: change 'Industry' to 'Principles' Change 'Industry' to 'Principles' May 12, 2021
@agarwal
Copy link
Member

agarwal commented May 12, 2021

I've generalized this issue to change the term everywhere.

@agarwal agarwal mentioned this issue May 12, 2021
Closed
@ghost ghost mentioned this issue May 13, 2021
Closed
5 tasks
This was referenced May 24, 2021
Merged
Closed
@avsm avsm closed this as completed in #376 May 25, 2021
avsm added a commit that referenced this issue May 25, 2021
@avsm
rename industry to principles
769620d 
Tweaks the menu text for the first two columns as well, still
working on the third one.

Closes #339
Sign up for free to subscribe to this conversation on GitHub. Already have an account? Sign in.
Assignees
No one assigned
Labels
Design-Implementation Request to implement a design suggestion good first issue Good for newcomers
Projects
None yet
Milestone
No milestone
Development

Successfully merging a pull request may close this issue.

rename industry to principles avsm/v3.ocaml.org
2 participants
@agarwal @ILeandersson