Option to shrink panel: updated doc and translation files

ChangeLog

@@ -1,10 +1,11 @@
-2016-10-02 master
+2016-10-08 master
 - Fixes:
   - tint2conf: executor tooltips are now correctly disabled when text config value is empty (contributed by Justin Jacobs)
 - Enhancements:
   - Desktop files (shortcuts) used in launcher are reloaded on click, in case the file has changed
   - New config option taskbar_hide_if_empty to hide an empty taskbar in multi_desktop mode (contributed by Benoit Averty)
   - Gradient backgrounds (contributed by Oskari Rauta)
+  - New option: panel_shrink (fixes issue #333)
 - New plugin: separator (contributed by Oskari Rauta)
 
 2016-08-02 0.12.12

doc/manual.html

@@ -451,7 +451,8 @@ panel_size = 94% 30
 </code></pre>
 
 <ul>
-<li><code>panel_margin = horizontal_margin vertical_margin</code> : The margins define the distance between the panel and the horizontal/vertical monitor edge. Use <code>0</code> to obtain a panel with the same size as the edge of the monitor (no margin).</li>
+<li><p><code>panel_shrink = boolean (0 or 1)</code> : If set to 1, the panel will shrink to a compact size dynamically.</p></li>
+<li><p><code>panel_margin = horizontal_margin vertical_margin</code> : The margins define the distance between the panel and the horizontal/vertical monitor edge. Use <code>0</code> to obtain a panel with the same size as the edge of the monitor (no margin).</p></li>
 </ul>
 <p><img src="images/panel_size_margin.jpg" alt=""></p>
 <ul>

doc/tint2.1

@@ -422,6 +422,8 @@ panel_size = 94% 30
 .RE
 .RS
 .IP \(bu 2
+\fB\fCpanel_shrink = boolean (0 or 1)\fR : If set to 1, the panel will shrink to a compact size dynamically.
+.IP \(bu 2
 \fB\fCpanel_margin = horizontal_margin vertical_margin\fR : The margins define the distance between the panel and the horizontal/vertical monitor edge. Use \fB\fC0\fR to obtain a panel with the same size as the edge of the monitor (no margin).
 .RE
 .PP

doc/tint2.md

@@ -351,6 +351,8 @@ panel_gradient_id = 5
 panel_size = 94% 30
 ```
 
+  * `panel_shrink = boolean (0 or 1)` : If set to 1, the panel will shrink to a compact size dynamically.
+
   * `panel_margin = horizontal_margin vertical_margin` : The margins define the distance between the panel and the horizontal/vertical monitor edge. Use `0` to obtain a panel with the same size as the edge of the monitor (no margin).
 
 ![](images/panel_size_margin.jpg)

src/tint2conf/properties.c

@@ -1387,7 +1387,7 @@ void create_panel(GtkWidget *parent)
 
 	row++;
 	col = 2;
-	label = gtk_label_new(_("Shrink"));
+	label = gtk_label_new(_("Compact"));
 	gtk_misc_set_alignment(GTK_MISC(label), 0, 0);
 	gtk_widget_show(label);
 	gtk_table_attach(GTK_TABLE(table), label, col, col+1, row, row+1, GTK_FILL, 0, 0, 0);