+void WriteVar (FILE* F, unsigned long V)
+/* Write a variable sized value to the file in special encoding */
+{
+ /* We will write the value to the file in 7 bit chunks. If the 8th bit
+ * is clear, we're done, if it is set, another chunk follows. This will
+ * allow us to encode smaller values with less bytes, at the expense of
+ * needing 5 bytes if a 32 bit value is written to file.
+ */
+ do {
+ unsigned char C = (V & 0x7F);
+ V >>= 7;
+ if (V) {
+ C |= 0x80;
+ }
+ Write8 (F, C);
+ } while (V != 0);
+}
+
+
+