diff --git a/INSTALL b/INSTALL new file mode 100644 index 000000000..83c11675a --- /dev/null +++ b/INSTALL @@ -0,0 +1,2 @@ +For installation instructions see the manual in the docs subdirectory +or online at . diff --git a/build.xml b/build.xml index 6c7d0cf5f..d735448a9 100644 --- a/build.xml +++ b/build.xml @@ -1011,6 +1011,7 @@ + @@ -1104,6 +1105,7 @@ +