From 2c6ea3c896e4fb9cb6162910d667b53262742b33 Mon Sep 17 00:00:00 2001
From: Nicola Fontana <ntd@entidi.it>
Date: Sun, 29 Dec 2013 14:01:31 +0100
Subject: [PATCH] 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 | 9 +--------
 nodist/symbols.mp | 2 ++
 2 files changed, 3 insertions(+), 8 deletions(-)

diff --git a/nodist/.gitignore b/nodist/.gitignore
index 16a1eccc..409a9192 100644
--- a/nodist/.gitignore
+++ b/nodist/.gitignore
@@ -1,11 +1,4 @@
 /adg.0
 /adg.log
-/symbols.0
-/symbols.1
-/symbols.2
-/symbols.3
-/symbols.4
-/symbols.5
-/symbols.6
-/symbols.7
+/*.mps
 /symbols.log
diff --git a/nodist/symbols.mp b/nodist/symbols.mp
index d6967e8d..7b074cc6 100644
--- a/nodist/symbols.mp
+++ b/nodist/symbols.mp
@@ -1,5 +1,7 @@
 % Miscellaneous symbols
 
+filenametemplate "%j-%c.mps";
+
 linecap := rounded;
 linejoin := rounded;
 
-- 
2.11.4.GIT