Merge branch 'master' into develop

2025-08-15 10:47:21 +00:00 · 2023-10-20 22:52:07 +02:00
parent 54e44299d8 038b89776d
commit 6161da3a22
3 changed files with 43 additions and 0 deletions
--- a/Development/docs-header.html
+++ b/Development/docs-header.html
@@ -0,0 +1,5 @@
+<head>
+<!-- Global site tag (gtag.js) - Google Analytics -->
+<script async src="https://www.googletagmanager.com/gtag/js?id=UA-97385487-1"></script>
+<script>window.dataLayer = window.dataLayer || [];function gtag(){dataLayer.push(arguments);}gtag('js', new Date());gtag('config', 'UA-97385487-1');</script>
+<meta name="viewport" content="width=device-width, initial-scale=1">
--- a/Development/docs-header.py
+++ b/Development/docs-header.py
@@ -0,0 +1,26 @@
+# import required module
+from pathlib import Path
+import os
+
+# assign directory
+directory = '.'
+
+print( "Replacing head tag in all html files" )
+
+# Read template file
+with open( os.path.dirname(__file__) + '/docs-header.html', 'r') as file:
+  newhead = file.read()
+
+# iterate over files in
+# that directory
+files = Path(directory).glob('*.html')
+for file in files:
+  # print(file)
+  with open(file, 'r') as fileread:
+    filedata = fileread.read()
+    # Replace the target string
+    filedata = filedata.replace( '<head>', newhead )
+
+  # Write the file out again
+  with open(file, 'w') as filewrite:
+    filewrite.write(filedata)