diff options
| author | Gaëtan Gilbert | 2017-12-16 10:58:52 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert | 2017-12-22 16:36:32 +0100 |
| commit | 87cbd64254f33439882156d9a297a6a2f6886057 (patch) | |
| tree | 8ffc7a81a0018c0a7d91c24871c84da00bea4996 /dev/set_raw_db | |
| parent | 50bd89748af03bb28ad7024f2ceef500489a91b0 (diff) | |
Cleanup debug printers a bit, add generated mli.
Diffstat (limited to 'dev/set_raw_db')
| -rw-r--r-- | dev/set_raw_db | 1 |
1 files changed, 0 insertions, 1 deletions
diff --git a/dev/set_raw_db b/dev/set_raw_db deleted file mode 100644 index 5caff7e5d4..0000000000 --- a/dev/set_raw_db +++ /dev/null @@ -1 +0,0 @@ -install_printer Top_printers.ppconstrdb |