nodist: generate symbols with .mps extension
[adg.git] / nodist / 
treea07d6dd5e386184a9af85497f9986ef6d4d9ef6e
drwxr-xr-x   ..
-rw-r--r-- 36 .gitignore
-rw-r--r-- 836 adg.mp
-rw-r--r-- 9630 adg.xcf.bz2
-rwxr-xr-x 1706 pre-commit
-rw-r--r-- 5069 symbols.mp