mirror of
https://github.com/MariaDB/server.git
synced 2025-01-19 05:22:25 +01:00
9 lines
186 B
HTML
9 lines
186 B
HTML
<html>
|
|
<head>
|
|
<title>Place holder for manual_toc.html</title>
|
|
</head>
|
|
<body>
|
|
This is just a place holder for the autogenerated manual_toc.html
|
|
to make "make dist" happy.
|
|
</body>
|
|
</html>
|