Fix the quotation in Fernando's modifications.

In a command like:
  mv $SOURCE $TARGET
the two arguments must be doublely quoted:
  mv "$SOURCE" "$TARGET"
That way, if $SOURCE is, for ex., "my file", it avoid the shell to call a
command like that:
  mv my file "$TARGET"
which is moving *two* files "my" and "file" to "$TARGET". With the
double-quotes, after the parameters substitution, the call is correct, with
only two arguments:
  mv "my file" "target"

Scripts/developer_scripts/autotest_cgal_with_cmake

@@ -247,7 +247,7 @@ EOF
         chmod ugo+x "${CGAL_BINARY_DIR}/localbuildscript.${1}"
         remote_command ${1} "${CGAL_BINARY_DIR}/localbuildscript.${1}" >> "${ACTUAL_LOGFILE}" 2>&1
                            
-      cp ${ACTUAL_LOGFILE} ${CGAL_BINARY_DIR}/installation.log.${1}
+      cp "${ACTUAL_LOGFILE}" "${CGAL_BINARY_DIR}/installation.log.${1}"
       
     done