Skip to content

Remove unused historyFile config property#253

Open
jordikroon wants to merge 1 commit into
php:masterfrom
jordikroon:config-historyfile
Open

Remove unused historyFile config property#253
jordikroon wants to merge 1 commit into
php:masterfrom
jordikroon:config-historyfile

Conversation

@jordikroon

Copy link
Copy Markdown
Member

This property doesn't seem to be used anymore.

@alfsb

alfsb commented Jun 8, 2026

Copy link
Copy Markdown
Member

@lacatoire lacatoire left a comment

Copy link
Copy Markdown
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Not related. That file is loaded via Config::$phpwebHistoryFilename (render.php / Package/PHP/Web.php). $historyFile is read nowhere and just shared the same default filename, so removing it is safe.

@alfsb

alfsb commented Jul 7, 2026

Copy link
Copy Markdown
Member

I asked because I'm interessed in moving all PhD stuffi into a separate genphdfiles.php, so doc-base/configure.php can be faster, by focusing only in joining and validating the XML files. In fact, I'm interessed in moving all PhD code into PhD repo.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

3 participants