equal
deleted
inserted
replaced
136 <script language="javascript" src="pygwt.js"></script> |
136 <script language="javascript" src="pygwt.js"></script> |
137 </body> |
137 </body> |
138 </html> |
138 </html> |
139 """ |
139 """ |
140 |
140 |
141 filename = os.path.split (source_file)[1] |
141 filename = os.path.split(source_file)[1] |
142 mod_name = os.path.splitext(filename)[0] |
142 mod_name = os.path.splitext(filename)[0] |
143 file_name = os.path.join (dest_path, mod_name + '.html') |
143 file_name = os.path.join(dest_path, mod_name + '.html') |
144 |
144 |
145 # if html file in output directory exists, leave it alone. |
145 # if html file in output directory exists, leave it alone. |
146 if os.path.exists (file_name): |
146 if os.path.exists (file_name): |
147 return 0 |
147 return 0 |
148 |
148 |