update lecture notes

2023-09-25 06:47:25 +02:00
parent bff99c3750
commit 097355ac7a
237 changed files with 50473 additions and 34642 deletions
@@ -35,7 +35,8 @@ div.highlight  {
    position: relative;
 }

-.highlight:hover button.copybtn {
+/* Show the copybutton */
+.highlight:hover button.copybtn, button.copybtn.success {
 	opacity: 1;
 }