From f8ce9b357f5bcff391cd2c9c39ef620d88539668 Mon Sep 17 00:00:00 2001
From: jvoisin <jvoisin@users.noreply.github.com>
Date: Fri, 5 Jan 2018 04:47:24 +0100
Subject: [PATCH] Change the priority for documentation tools (#1980)

---
 src/apps.json | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/apps.json b/src/apps.json
index 077da2a98..5f7666909 100644
--- a/src/apps.json
+++ b/src/apps.json
@@ -12143,7 +12143,7 @@
     },
     "4": {
       "name": "Documentation Tools",
-      "priority": "9"
+      "priority": "2"
     },
     "5": {
       "name": "Widgets",