diff options
| author | Hugo Herbelin | 2020-04-13 16:50:41 +0200 |
|---|---|---|
| committer | Lysxia | 2020-04-20 10:38:29 -0400 |
| commit | 3b5937c66704c2ab4643442dc3296198b33006e5 (patch) | |
| tree | d92855b011dab712d57ea76d3af8be7abfcf3146 /tools | |
| parent | 078e6c6d27bc3a13bb9e7ac6c9c5b8e05450af80 (diff) | |
Adding highlighting of the target of a internal link in coqdoc CSS.
Co-Authored-By: Xia Li-yao <Lysxia@users.noreply.github.com>
Diffstat (limited to 'tools')
| -rw-r--r-- | tools/coqdoc/coqdoc.css | 5 |
1 files changed, 5 insertions, 0 deletions
diff --git a/tools/coqdoc/coqdoc.css b/tools/coqdoc/coqdoc.css index 2c2bd98541..48096e555a 100644 --- a/tools/coqdoc/coqdoc.css +++ b/tools/coqdoc/coqdoc.css @@ -331,3 +331,8 @@ ul.doclist { margin-top: 0em; margin-bottom: 0em; } + +.code :target { + border: 2px solid #D4D4D4; + background-color: #e5eecc; +} |
