From 996295e82f6aac57130889eea42dc857e81ca83e Mon Sep 17 00:00:00 2001
From: logmanoriginal <logmanoriginal@users.noreply.github.com>
Date: Wed, 26 Sep 2018 19:58:24 +0200
Subject: [PATCH] Add 'dev.' to the release version in master

This helps (roughly) identifying versions when opening issues on
GitHub, using the latest ZIP file for master.

References #773
---
 lib/Configuration.php | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/lib/Configuration.php b/lib/Configuration.php
index 352f782d..e89c8445 100644
--- a/lib/Configuration.php
+++ b/lib/Configuration.php
@@ -1,7 +1,7 @@
 <?php
 class Configuration {
 
-	public static $VERSION = '2018-09-09';
+	public static $VERSION = 'dev.2018-09-09';
 
 	public static $config = null;