svgui/svgui.py
changeset 1833 2269739dd098
parent 1832 0f1081928d65
child 1850 614396cbffbf
equal deleted inserted replaced
1832:0f1081928d65 1833:2269739dd098
    84         @return: [(C_file_name, CFLAGS),...] , LDFLAGS_TO_APPEND
    84         @return: [(C_file_name, CFLAGS),...] , LDFLAGS_TO_APPEND
    85         """
    85         """
    86 
    86 
    87         current_location = self.GetCurrentLocation()
    87         current_location = self.GetCurrentLocation()
    88         # define a unique name for the generated C file
    88         # define a unique name for the generated C file
    89         location_str = "_".join(map(lambda x: str(x), current_location))
    89         location_str = "_".join(map(str, current_location))
    90 
    90 
    91         res = ([], "", False)
    91         res = ([], "", False)
    92 
    92 
    93         svgfile = self._getSVGpath()
    93         svgfile = self._getSVGpath()
    94         if os.path.exists(svgfile):
    94         if os.path.exists(svgfile):