org: uses nice dot arrows
Suggested by Akim Demaille. Fixes #69. * doc/org/.dir-locals.el, doc/org/init.el.in, wrap/python/tests/automata.ipynb: Set arrowhead and arrowsize. * doc/org/autfilt.org, doc/org/dstar2tgba.org, doc/org/ltl2tgba.org, doc/org/oaut.org: Adjust.
This commit is contained in:
parent
30b8788676
commit
8e6b35e5e3
7 changed files with 352 additions and 350 deletions
|
|
@ -25,7 +25,8 @@
|
|||
(concat "PATH=@abs_top_builddir@/src/bin" path-separator "$PATH sh"))
|
||||
|
||||
(setenv "SPOT_DOTDEFAULT" "brf(Lato)")
|
||||
(setenv "SPOT_DOTEXTRA" "node[style=filled, fillcolor=\"#ffffa0\"]")
|
||||
(setenv "SPOT_DOTEXTRA"
|
||||
"node[style=filled, fillcolor=\"#ffffa0\"] edge[arrowhead=vee, arrowsize=.7]")
|
||||
|
||||
(setq org-export-html-home/up-format
|
||||
"<div id=\"org-div-home-and-up\" style=\"text-align:center;white-space:nowrap;\">
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue