From 74b33e4dfc7b646ffc528f5c580541cbd32fa32c Mon Sep 17 00:00:00 2001
From: Oliver Bock <oliver.bock@aei.mpg.de>
Date: Wed, 13 Jan 2016 15:55:39 +0100
Subject: [PATCH] HTML: Make platforms accessible to Drupal by declaring it as
 global

---
 html/inc/result.inc | 1 +
 1 file changed, 1 insertion(+)

diff --git a/html/inc/result.inc b/html/inc/result.inc
index 7d1c228a69..5267046c27 100644
--- a/html/inc/result.inc
+++ b/html/inc/result.inc
@@ -24,6 +24,7 @@ require_once("../inc/common_defs.inc");
 //
 global $apps;
 global $app_versions;
+global $platforms;
 $apps = array();
 $app_versions = array();
 $platforms = array();