aboutsummaryrefslogtreecommitdiffstats
path: root/Makefile
diff options
context:
space:
mode:
Diffstat (limited to 'Makefile')
-rw-r--r--Makefile5
1 files changed, 4 insertions, 1 deletions
diff --git a/Makefile b/Makefile
index 3ff20a6..3b51d00 100644
--- a/Makefile
+++ b/Makefile
@@ -87,7 +87,10 @@ clean:: Makefile.coq
rm -f Makefile.coq
detangle-all:
- emacs --batch --eval "(progn(require 'org)(require 'ob-tangle)$(foreach vs,$(VS),(org-babel-detangle \"$(vs)\")))"
+ emacs --batch --eval "(progn(require 'org)(require 'ob-tangle)\
+ (setq org-src-preserve-indentation t)\
+ $(foreach vs,$(VS),(org-babel-detangle \"$(vs)\"))\
+ (org-save-all-org-buffers))"
clean::
rm -f */*.v.d */*.glob */*.vo */*~ *~