From e9894ffb7777c6cc73100bd3339a4174bd3b9155 Mon Sep 17 00:00:00 2001
From: Bryn Edwards <bryn@protonmail.ch>
Date: Mon, 17 Jul 2017 06:51:20 +0100
Subject: [PATCH] Fix #249 (#655)
---
haddock-api/resources/html/Classic.theme/xhaddock.css | 1 +
haddock-api/resources/html/Ocean.std-theme/ocean.css | 1 +
2 files changed, 2 insertions(+)
diff --git a/haddock-api/resources/html/Classic.theme/xhaddock.css b/haddock-api/resources/html/Classic.theme/xhaddock.css
index 19dc28ec66..1bf668e96e 100644
--- a/haddock-api/resources/html/Classic.theme/xhaddock.css
+++ b/haddock-api/resources/html/Classic.theme/xhaddock.css
@@ -285,6 +285,7 @@ div.top h5 {
padding: 0 8px 2px 5px;
margin-right: -3px;
background-color: #f0f0f0;
+ -moz-user-select: none;
}
div.subs {
diff --git a/haddock-api/resources/html/Ocean.std-theme/ocean.css b/haddock-api/resources/html/Ocean.std-theme/ocean.css
index 3bfc8982ac..8d3f91a9ca 100644
--- a/haddock-api/resources/html/Ocean.std-theme/ocean.css
+++ b/haddock-api/resources/html/Ocean.std-theme/ocean.css
@@ -394,6 +394,7 @@ div#style-menu-holder {
background: #f0f0f0;
padding: 0 0.5em 0.2em;
margin: 0 -0.5em 0 0;
+ -moz-user-select: none;
}
#interface .src .selflink {
border-left: 1px solid #919191;
--
GitLab