nodist: generate symbols with .mps extension
commit2c6ea3c896e4fb9cb6162910d667b53262742b33
authorNicola Fontana <ntd@entidi.it>
Sun, 29 Dec 2013 13:01:31 +0000 (29 14:01 +0100)
committerNicola Fontana <ntd@entidi.it>
Sun, 29 Dec 2013 13:03:07 +0000 (29 14:03 +0100)
treec399b4d5944d42ef4895c7a439f6d41c0d19a50a
parent164d442e7c4fadce5cee35c4a9414b4653b5481f
nodist: generate symbols with .mps extension

To import graphics into LaTeX in an easier way, change the template file
name generation in the MetaPost file to a more useful way.
nodist/.gitignore
nodist/symbols.mp