From 2b715208c0a681476048cfead0902811e4a313e9 Mon Sep 17 00:00:00 2001
From: Vincent Wei <vincent@minigui.org>
Date: Sat, 14 Mar 2020 22:28:47 +0800
Subject: [PATCH] add double_buffering key to drm section

---
 etc/MiniGUI.cfg | 4 ++++
 1 file changed, 4 insertions(+)

diff --git a/etc/MiniGUI.cfg b/etc/MiniGUI.cfg
index 09efbdc0..c2d8d3ae 100644
--- a/etc/MiniGUI.cfg
+++ b/etc/MiniGUI.cfg
@@ -72,6 +72,10 @@ device=/dev/dri/card0
 # The default value is 96.
 dpi=96
 
+# Whether double buffering is enabled.
+# Since 5.0.0.
+double_buffering=true
+
 # The filename of the shared library for the external driver.
 # The equivalent environment variable: MG_GAL_DRM_DRIVER
 exdriver=libhidrmdrivers.so.0