fix: make line number not selectable

fkie-cad · Dec 2, 2024 · 8673795 · 8673795
1 parent 2e64e4c
commit 8673795
Showing 1 changed file with 2 additions and 2 deletions.
diff --git a/src/web_interface/static/css/line_numbering.css b/src/web_interface/static/css/line_numbering.css
@@ -5,10 +5,10 @@
 
 #preview-div pre .line-number {
   float:left;
-  margin: 0;
   border-right:1px solid;
   text-align:right;
-  margin-right: 1em;
+  margin: 0 1em 0 0;
+  user-select: none;
 }
 
 #preview-div pre .line-number span {