From 3ad6817cd1c8b3ecd23ce8a8d1a9eece831f487f Mon Sep 17 00:00:00 2001
From: Neels Hofmeyr <neels@hofmeyr.de>
Date: Wed, 6 Mar 2019 16:48:50 +0100
Subject: [PATCH] add manuals.opts, no_doxygen.opts, no_optimization.opts

Change-Id: Ief9e6865eaff587dbd1f1f73f2fecac470e77a81
---
 manuals.opts         | 1 +
 no_doxygen.opts      | 1 +
 no_optimization.opts | 1 +
 3 files changed, 3 insertions(+)
 create mode 100644 manuals.opts
 create mode 100644 no_doxygen.opts
 create mode 100644 no_optimization.opts

diff --git a/manuals.opts b/manuals.opts
new file mode 100644
index 0000000..2ba5237
--- /dev/null
+++ b/manuals.opts
@@ -0,0 +1 @@
+ALL --enable-manuals
diff --git a/no_doxygen.opts b/no_doxygen.opts
new file mode 100644
index 0000000..b2aa682
--- /dev/null
+++ b/no_doxygen.opts
@@ -0,0 +1 @@
+ALL --disable-doxygen
diff --git a/no_optimization.opts b/no_optimization.opts
new file mode 100644
index 0000000..3d85054
--- /dev/null
+++ b/no_optimization.opts
@@ -0,0 +1 @@
+ALL CFLAGS="-g -O0"