this repo has no description
1
fork

Configure Feed

Select the types of activity you want to include in your feed.

Revert "Add admonition styling to odoc CSS and cleanup deprecated/dune"

This reverts commit dcda8e8d329551c8b6e41927ef9147eabad53964.

+6 -34
+6 -2
doc/deprecated/dune
··· 1 - ; This directory's mld files are included via the parent doc/dune documentation stanza. 2 - ; No separate install stanza needed. 1 + (install 2 + (section doc) 3 + (files 4 + (parent_child_spec.mld as odoc-pages/deprecated/parent_child_spec.mld) 5 + (index.mld as odoc-pages/deprecated/index.mld)) 6 + (package odoc))
-32
src/html_support_files/odoc.css
··· 770 770 .at-tags li { padding-left: 3ex; text-indent: -3ex; } 771 771 .at-tags .at-tag { text-transform: capitalize } 772 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 773 /* Alert emoji */ 806 774 807 775 .alert::before, .deprecated::before {