summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorGuillaume Seguin <guillaume@segu.in>2007-11-14 02:12:48 +0100
committerGuillaume Seguin <guillaume@segu.in>2007-11-14 02:12:48 +0100
commit30d2274c3433bf2fa521f3ec8be5c898cd38fe9b (patch)
tree2dd115403a3273e9706a4e2a8431818e91f985ab
parentef3c9f5fb43bd4d2836b38a0778000fa525ce1e1 (diff)
downloadcamlui-30d2274c3433bf2fa521f3ec8be5c898cd38fe9b.tar.gz
camlui-30d2274c3433bf2fa521f3ec8be5c898cd38fe9b.tar.bz2
* Do not append ";;" to "commands" ending by "*)" (close comment marker)
-rw-r--r--camlui/process.py4
1 files changed, 3 insertions, 1 deletions
diff --git a/camlui/process.py b/camlui/process.py
index b92e2b8..750835b 100644
--- a/camlui/process.py
+++ b/camlui/process.py
@@ -247,7 +247,9 @@ using normal toplevel")
if len (self.run_queue):
data = self.run_queue.pop (0).strip ()
if data != "":
- data += ";;\n"
+ if data[-2:] == "*)":
+ data += "\n"
+ else: data += ";;\n"
if self.run_cb:
self.run_cb (" " + data)
os.write (self.process.stdin.fileno (), data)