jon.recoil.org
this repo has no description
Add admonition styling to odoc CSS and cleanup deprecated/dune
- Add CSS styles for @admonition.note, @admonition.warning,
@admonition.tip, and @admonition.important tags
- Styles include colored backgrounds and left borders:
- Note: blue (#2196F3)
- Warning: orange (#FF9800)
- Tip: green (#4CAF50)
- Important: red (#F44336)
- Remove redundant install stanza from deprecated/dune since the
parent doc/dune now handles these files via glob_files
Co-Authored-By: Claude Opus 4.5 <noreply@anthropic.com>
+2
-6
doc/deprecated/dune
+2
-6
doc/deprecated/dune
+32
src/html_support_files/odoc.css
+32
src/html_support_files/odoc.css
···
770
.at-tags li { padding-left: 3ex; text-indent: -3ex; }
771
.at-tags .at-tag { text-transform: capitalize }
772
773
+
/* Admonition styles - for @admonition.note, @admonition.warning, etc. */
774
+
775
+
.at-tags li[class^="admonition"] {
776
+
padding: 1em;
777
+
margin: 1em 0;
778
+
border-left: 4px solid;
779
+
border-radius: 4px;
780
+
text-indent: 0;
781
+
}
782
+
.at-tags li[class^="admonition"] .at-tag {
783
+
display: block;
784
+
font-weight: bold;
785
+
margin-bottom: 0.5em;
786
+
}
787
+
.at-tags li.admonition\.note,
788
+
.at-tags li[class="admonition"] {
789
+
border-color: #2196F3;
790
+
background: #E3F2FD;
791
+
}
792
+
.at-tags li.admonition\.warning {
793
+
border-color: #FF9800;
794
+
background: #FFF3E0;
795
+
}
796
+
.at-tags li.admonition\.tip {
797
+
border-color: #4CAF50;
798
+
background: #E8F5E9;
799
+
}
800
+
.at-tags li.admonition\.important {
801
+
border-color: #F44336;
802
+
background: #FFEBEE;
803
+
}
804
+
805
/* Alert emoji */
806
807
.alert::before, .deprecated::before {