2
0
mirror of https://github.com/boostorg/website.git synced 2026-02-02 09:22:19 +00:00
Files
website/site-tools/update-doc-list.php
2012-02-04 13:58:23 +00:00

9 lines
279 B
PHP

<?php
echo "Serializing library info\n";
require_once(dirname(__FILE__) . '/../common/code/boost_libraries.php');
$libs = new boost_libraries(dirname(__FILE__) . '/../doc/libraries.xml');
file_put_contents(dirname(__FILE__) . '/../generated/libraries.txt', serialize($libs));