TOOLS/fil2string.py: fix for use with binary files

The script was written to be able to deal with binary files, but it had
a bug corrupting some data: e.g. a byte sequence 0x1 0x37 was printed as
"\17" (0x1 = escaped as "\1", and 0x37 = kept as literal "7"), which
would be interpreted as single character 0xF.

Always pad octal literals to length 3, which makes the escape sequences
unambiguous.

TOOLS/file2string.py

@@ -8,7 +8,7 @@
 import sys
 
 def main(infile):
-    conv = ['\\' + oct(c)[2:] for c in range(256)]
+    conv = ['\\' + ("%03o" % c) for c in range(256)]
     safe_chars = "ABCDEFGHIJKLMNOPQRSTUVWXYZabcdefghijklmnopqrstuvwxyz" \
                  "0123456789!#%&'()*+,-./:;<=>?[]^_{|}~ "
     for c in safe_chars: