7.15.2 release

JeroenDeDauw · JeroenDeDauw · commit fad8b358058b · 2019-12-24T13:07:53.000+01:00
diff --git a/RELEASE-NOTES.md b/RELEASE-NOTES.md
@@ -3,6 +3,12 @@ different releases and which versions of PHP and MediaWiki they support, see the
 [platform compatibility tables](INSTALL.md#platform-compatibility-and-release-status).
 
 
+## Maps 7.15.2
+
+Released on December 24th, 2019.
+
+* Improved reliability of Leaflet resource loading
+
 ## Maps 7.15.1
 
 Released on December 23rd, 2019.
diff --git a/extension.json b/extension.json
@@ -1,6 +1,6 @@
 {
 	"name": "Maps",
-	"version": "7.15.1",
+	"version": "7.15.2",
 
 	"author": [
 		"[https://www.entropywins.wtf/mediawiki Jeroen De Dauw]",

Original file line number	Diff line number	Diff line change
`@@ -1,6 +1,6 @@`
`1`	`1`	`{`
`2`	`2`	`"name": "Maps",`
`3`		`- "version": "7.15.1",`
	`3`	`+ "version": "7.15.2",`
`4`	`4`
`5`	`5`	`"author": [`
`6`	`6`	`"[https://www.entropywins.wtf/mediawiki Jeroen De Dauw]",`