Skip to content
New issue

Have a question about this project? # for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “#”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? # to your account

Doc: manual - remove useless span tag #4513

Merged
merged 2 commits into from
Mar 19, 2021

Conversation

dannywillems
Copy link
Contributor

Looks like there is no class opam. It also prints the span tag sometimes in the manual, see https://opam.ocaml.org/doc/Manual.html

@rjbou
Copy link
Collaborator

rjbou commented Jan 28, 2021

The class is defined at the beginning of the file, added in #2665 :

<style type="text/css"><!--
  .opam {font-family: Tahoma,Verdana,sans-serif; font-size: 110%; font-weight: lighter; line-height: 90.9%}
--></style>

but commented ? ping @AltGr if you remember what you did 5 years ago :D

@dannywillems
Copy link
Contributor Author

The class is defined at the beginning of the file, added in #2665 :

<style type="text/css"><!--
  .opam {font-family: Tahoma,Verdana,sans-serif; font-size: 110%; font-weight: lighter; line-height: 90.9%}
--></style>

but commented ? ping @AltGr if you remember what you did 5 years ago :D

My bad for the definition... I simply checked in the browser console and run a substitute to remove the span 👀 .

@rjbou
Copy link
Collaborator

rjbou commented Jan 28, 2021

But it highlights the issue, it shouldn't be verbatim in the html...

@rjbou rjbou added AREA: DOCUMENTATION PR: WIP Not for merge at this stage labels Jan 28, 2021
@AltGr
Copy link
Member

AltGr commented Mar 19, 2021

Yeah, that dates back from when we renamed OPAM to opam. I wanted to make it still stick out a little, but I think gave up on the CSS because of a limitation in markdown or something. I don't think this is actually needed (we lived without it for 5 years ;) ), thanks for the contribution!

@AltGr AltGr merged commit 9f9e929 into ocaml:master Mar 19, 2021
# for free to join this conversation on GitHub. Already have an account? # to comment
Labels
AREA: DOCUMENTATION PR: WIP Not for merge at this stage
Projects
None yet
Development

Successfully merging this pull request may close these issues.

3 participants