From e9894ffb7777c6cc73100bd3339a4174bd3b9155 Mon Sep 17 00:00:00 2001 From: Bryn Edwards Date: Mon, 17 Jul 2017 06:51:20 +0100 Subject: Fix #249 (#655) --- haddock-api/resources/html/Ocean.std-theme/ocean.css | 1 + 1 file changed, 1 insertion(+) (limited to 'haddock-api/resources/html/Ocean.std-theme') diff --git a/haddock-api/resources/html/Ocean.std-theme/ocean.css b/haddock-api/resources/html/Ocean.std-theme/ocean.css index 3bfc8982..8d3f91a9 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; -- cgit v1.2.3