adjust shortcut div width styles to adapt to different numbers of tools

diff --git a/docs/themes/default/styles.css b/docs/themes/default/styles.css
index 768a8f7..19292ba 100644 (file)
--- a/docs/themes/default/styles.css
+++ b/docs/themes/default/styles.css
@@ -1212,7 +1212,7 @@ div#shortcuts{
        border-radius: 0em 0em .5em .5em;;
        -moz-border-radius: 0em 0em .5em .5em;
        float:right;
-       width:12em;
+
        margin-right:2em;
        padding:.1em;
 }