From bf8e57e5377bf6a6eaac3131f041a931cb563ec2 Mon Sep 17 00:00:00 2001 From: Jordi Kroon Date: Sun, 26 Jul 2026 21:42:30 +0200 Subject: [PATCH] change manual configuration entity file extension from .inc to .ent --- configure.php | 2 +- manual.xml | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/configure.php b/configure.php index 047299e8c8..bd17307952 100755 --- a/configure.php +++ b/configure.php @@ -595,7 +595,7 @@ function dtd_conf_entities() else $conf[] = ""; - file_put_contents( __DIR__ . "/temp/manual.inc" , implode( "\n" , $conf ) ); + file_put_contents( __DIR__ . "/temp/manual.ent" , implode( "\n" , $conf ) ); } function dtd_file_entities() diff --git a/manual.xml b/manual.xml index c8a3521703..42ce09da9d 100644 --- a/manual.xml +++ b/manual.xml @@ -2,7 +2,7 @@ - + %configure;