wb_load files, backslash replaced by double backslash to void parse errors

wb/lib/wb/src/wb_print_wbl.cpp

@@ -644,6 +644,8 @@ void wb_print_wbl::printText(wb_volume& v,
   for (ip = text, i = 0; *ip != 0 && i < end; ip++) {
     if (*ip == '"')
       m_os << "\\";
+    else if (*ip == '\\')
+      m_os << "\\";
     m_os << *ip;
   }
     

wb/lib/wb/src/wb_wblnode.cpp

@@ -1888,11 +1888,13 @@ void wb_wblnode::registerNode( wb_vrepwbl *vol)
   }
   else if (getType() == tokens.STRING_LITERAL)
   {
-    // Remove quotes and replace \" with "
+    // Remove quotes and replace \" with " and also backslash
     char str[2048];
     const char *s;
     char *t;
     bool first = true;
+    bool backslash_done = false;
+
     t = str;
     for ( s = getText().c_str(); *s; s++) {
       if ( first) {
@@ -1901,6 +1903,12 @@ void wb_wblnode::registerNode( wb_vrepwbl *vol)
       }
       if ( *s == '"' && *(s-1) == '\\')
         t--;
+      if ( *s == '\\' && *(s-1) == '\\' && !backslash_done) {
+	backslash_done = true;
+        t--;
+      }
+      else
+	backslash_done = false;
       *t = *s;
       t++;
     }