search

php / doc-base

Tools for the PHP documentation
Other
343 stars 85 forks source link

Generate sources.xml #38

Closed salathe closed 3 years ago

salathe commented 3 years ago

See also php/phd#55 and php/web-php#434

The new sources.xml file contains the mapping from an XML ID to the source XML file that declares it.

Generation of the sources.xml file is enabled by default. To disable it, run configure.php with the --disable-sources-file option.

Example of sources.xml contents:

<?xml version="1.0"?>
<sources>
  <item
    id="extensions.membership"
    lang="en"
    path="appendices/extensions.xml"/>
  <item
    id="extensions.membership.core"
    lang="en"
    path="appendices/extensions.xml"/>
  ...
</sources>