From d39fc735ba03fe538e3f5c41511fec610ab83910 Mon Sep 17 00:00:00 2001
From: Jordi Kroon <jkroon@onyourmarks.agency>
Date: Mon, 8 Jun 2026 00:07:19 +0200
Subject: [PATCH] remove unused historyFile config property

---
 phpdotnet/phd/Config.php | 1 -
 1 file changed, 1 deletion(-)

diff --git a/phpdotnet/phd/Config.php b/phpdotnet/phd/Config.php
index defc50c6..82811383 100644
--- a/phpdotnet/phd/Config.php
+++ b/phpdotnet/phd/Config.php
@@ -13,7 +13,6 @@ class Config
     public bool $noToc = false;
     public string $xmlRoot = '.';
     public string $xmlFile = './.manual.xml';
-    public string $historyFile = './fileModHistory.php';
     public string $langDir = './';
     public string $language = 'en';
     public string $fallbackLanguage = 'en';