From 1187d01a79748632a593d41815bebf612ae67935 Mon Sep 17 00:00:00 2001
From: Bruno Alla <alla.brunoo@gmail.com>
Date: Mon, 15 Dec 2025 15:51:50 +0000
Subject: [PATCH] Make "Copy" button smaller

---
 docs_theme/js/copy-button.js | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/docs_theme/js/copy-button.js b/docs_theme/js/copy-button.js
index 667460c8b..979c8a962 100644
--- a/docs_theme/js/copy-button.js
+++ b/docs_theme/js/copy-button.js
@@ -1,7 +1,7 @@
 document.addEventListener("DOMContentLoaded", function () {
   document.querySelectorAll("pre > code").forEach(function (codeBlock) {
     const button = document.createElement("button");
-    button.className = "copy-block-button btn btn-inverse btn-small";
+    button.className = "copy-block-button btn btn-inverse btn-mini";
     button.type = "button";
     button.textContent = "Copy";