From mboxrd@z Thu Jan 1 00:00:00 1970 Received: (from weis@localhost) by pauillac.inria.fr (8.7.6/8.7.3) id IAA28531 for caml-redistribution; Fri, 15 Oct 1999 08:39:08 +0200 (MET DST) Received: from nez-perce.inria.fr (nez-perce.inria.fr [192.93.2.78]) by pauillac.inria.fr (8.7.6/8.7.3) with ESMTP id VAA05390 for ; Thu, 14 Oct 1999 21:33:24 +0200 (MET DST) Received: from beach.frankfurt.netsurf.de (beach.frankfurt.netsurf.de [194.64.181.2]) by nez-perce.inria.fr (8.8.7/8.8.7) with ESMTP id VAA05685 for ; Thu, 14 Oct 1999 21:33:22 +0200 (MET DST) Received: from ice.darmstadt.netsurf.de (board-123.darmstadt.netsurf.de [194.163.86.251]) by beach.frankfurt.netsurf.de (8.8.5/8.8.5) with ESMTP id VAA09494; Thu, 14 Oct 1999 21:33:18 +0200 (MET DST) Received: from localhost (localhost [[UNIX: localhost]]) by ice.darmstadt.netsurf.de (8.9.3/8.9.3) id VAA20267; Thu, 14 Oct 1999 21:24:00 +0200 From: Gerd Stolpmann Reply-To: Gerd.Stolpmann@darmstadt.netsurf.de Organization: privat To: Juergen Pfitzenmaier Subject: Re: Quotes inside a comment ? Date: Thu, 14 Oct 1999 21:17:49 +0200 X-Mailer: KMail [version 1.0.21] Content-Type: text/plain References: <199910131230.OAA15829@sunstroke.informatik.uni-tuebingen.de> Cc: caml-list@inria.fr MIME-Version: 1.0 Message-Id: <99101421240000.20232@ice> Content-Transfer-Encoding: 8bit Sender: weis On Wed, 13 Oct 1999, Juergen Pfitzenmaier wrote: >The documentation says even inside comments the quotes (that's -- " --) >have to be used pairwise. Is there any reason for this ? To comment code out, e.g. (* print_string "*)" *) >I would like to have a good documentation for the code I write and my >preferred way is to use nuweb and put some TeX right beside the piece >of code it refers to. But sometimes I have to use a non-english language >for the comments and then I need special characters that are constructed >with a -- " -- in front of them. If it is Latex why don't you use the inputenc package? If not, I don't have an easy answer. Gerd -- ---------------------------------------------------------------------------- Gerd Stolpmann Telefon: +49 6151 997705 (privat) Viktoriastr. 100 64293 Darmstadt EMail: Gerd.Stolpmann@darmstadt.netsurf.de (privat) Germany ----------------------------------------------------------------------------