From: fennecdjay <astor.jeremie@wanadoo.fr>
Date: Wed, 19 Jun 2019 23:24:31 +0000 (+0200)
Subject: :art: Update
X-Git-Tag: nightly~2428^2
X-Git-Url: http://10.10.0.4:5575/?a=commitdiff_plain;h=refs%2Fpull%2F126%2Fhead;p=gwion.git

:art: Update
---

diff --git a/.gitignore b/.gitignore
index 77ccf339..3b548b3c 100644
--- a/.gitignore
+++ b/.gitignore
@@ -2,5 +2,4 @@ gwion
 .d
 config.mk
 include/generated.h
-docs/WIP_*.md
 .desk
diff --git a/Makefile b/Makefile
index cd7ed00a..64258ff9 100644
--- a/Makefile
+++ b/Makefile
@@ -109,5 +109,4 @@ test:
 include $(wildcard .d/*.d)
 include util/target.mk
 include util/intl.mk
-include docs/config.mk
 include docs.mk
diff --git a/docs.mk b/docs.mk
index 1dd0e686..90f3c9cc 100644
--- a/docs.mk
+++ b/docs.mk
@@ -59,3 +59,22 @@ _noterm_header=echo '<blockquote><p style=$(CSS)>'
 _noterm_test=$(call _test_check) && $(call _noterm_status)
 _noterm_footer=echo '</p></blockquote>'
 _noterm=($(call _noterm_header); $(call _noterm_log); $(call _noterm_test); $(call _noterm_footer))
+DOCTOOL ?= mkdocs
+
+# output box css
+BACKGROUND    = background-color:\#e3e3e3;
+BORDER        = border: 5px solid \#343131;
+PADDING       = padding: 10px;
+MARGIN        = margin-right: 20%; margin-left: 20%;
+BORDER_RADIUS = -moz-border-radius: 15px; -webkit-border-radius: 15px;
+CSS           = "$(BACKGROUND) $(BORDER) $(PADDING) $(MARGIN) $(BORDER_RADIUS)"
+
+VALGRIND     ?= valgrind
+VALGRIND_LOG ?= vlog
+VALGRIND_OPT += --leak-check=yes --log-file=${VALGRIND_LOG}
+
+INTERM_OK       = \033[32mOK\033[0m
+INTERM_NOT_OK   = \033[31mNOT OK\033[0m
+
+NOTERM_OK= &\#10004;
+NOTERM_NOT_OK= &\#10008;