<html>
<head>
<meta content="text/html; charset=UTF-8" http-equiv="Content-Type">
</head>
<body bgcolor="#FFFFFF" text="#000000">
I've pushed Patrick's additions to the public repo. David, it's a
slightly different naming convention than yours, but it should serve
the same purpose. Let me know if some further compensating changes
are needed to add functionality that you added in a different way.<br>
<br>
<div class="moz-cite-prefix">On 05/26/2014 02:07 PM, Patrick Hurst
wrote:<br>
</div>
<blockquote
cite="mid:CAGG20NqrW_=9==tH7Ajf_zn9EiDOW2O_pfKEHsOZ14AkivxRxA@mail.gmail.com"
type="cite">
<div dir="ltr">I actually have a commit that I apparently only
pushed to my local copy of the repository (it's accessible at <a
moz-do-not-send="true"
href="http://web.mit.edu/%7Ephurst/hg/bootstrap/">http://web.mit.edu/~phurst/hg/bootstrap/</a>
or the corresponding Athena AFS path) that splits out Bootstrap
2 and Bootstrap 3 into separate files; in Bootstrap 3 (the one
I've been using), the convention I used is to prefix conflicting
names with bs3 (so bs3-h1, bs3-h2, etc.). I personally think the
benefit of not having to play renaming games with the tag names
is worth the small downside of not being able to directly
copy-paste code in, since any errors will show up at compile
time.</div>
<div class="gmail_extra"><br>
<br>
<div class="gmail_quote">On Mon, May 26, 2014 at 9:55 AM, Adam
Chlipala <span dir="ltr"><<a moz-do-not-send="true"
href="mailto:adamc@csail.mit.edu" target="_blank">adamc@csail.mit.edu</a>></span>
wrote:<br>
<blockquote class="gmail_quote" style="margin:0 0 0
.8ex;border-left:1px #ccc solid;padding-left:1ex">
<div class="">On 05/25/2014 06:45 PM, David Snider wrote:<br>
<blockquote class="gmail_quote" style="margin:0 0 0
.8ex;border-left:1px #ccc solid;padding-left:1ex">
Some of the style names were conflicting with basis tag
names. There might be more but I fixed the ones I found.
Attached is a patch.<br>
</blockquote>
<br>
</div>
I believe Patrick Hurst, the author of that code, was aware
of that problem, so I'd like to hear from him first, about
what he thinks of this patch. One downside is that
off-the-shelf HTML code using normal Bootstrap wouldn't be
usable directly.<br>
</blockquote>
</div>
<br>
</div>
</blockquote>
<br>
</body>
</html>