diff --git a/docs/manual/BUILDING b/docs/manual/BUILDING new file mode 100644 index 00000000000..71ad9458bcb --- /dev/null +++ b/docs/manual/BUILDING @@ -0,0 +1,2 @@ +For instructions on building the manual, see +.