Skip to content
GitLab
Menu
Projects
Groups
Snippets
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in
Toggle navigation
Menu
Open sidebar
cduce
cduce
Commits
6a3e3df5
Commit
6a3e3df5
authored
Oct 05, 2007
by
Pietro Abate
Browse files
[r2003-05-21 21:53:45 by cvscast] reverted back php_css Beppe
Original author: cvscast Date: 2003-05-21 21:53:45+00:00
parent
f8e5b9de
Changes
1
Hide whitespace changes
Inline
Side-by-side
web/site.cd
View file @
6a3e3df5
...
...
@@ -101,6 +101,25 @@ let fun protect_quote (s : String) : String =
transform s with '"' -> [ '\\"' ] | c -> [c];;
let php_css : String =
['
<?php
$browser = getenv("HTTP_USER_AGENT");
if (preg_match("/MSIE/i", "$browser")) {
$css = "<link rel=\\"stylesheet\\" href=\\"cduce.css\\"
type=\\"text/css\\">";
} elseif (preg_match("/Mozilla/i", "$browser")) {
$css = "<blink>For better presentation use a more recent version
of your browser, like Netscape 6</blink>";
} if (preg_match("/Mozilla\\/5.0/i", "$browser")) {
$css = "<link rel=\\"stylesheet\\" href=\\"cduce.css\\"
type=\\"text/css\\">";
} elseif (preg_match("/opera/i", "$browser")) {
$css = "<link rel=\\"stylesheet\\" href=\\"cduce.css\\"
type=\\"text/css\\">";
}
echo "$css";
?>
'];;
(** It does not work with IE
if php then
['
<?php $browser = getenv("HTTP_USER_AGENT");
if (preg_match("/Mozilla/i", "$browser") && !preg_match("/Mozilla\\/5.0/i", "$browser"))
...
...
@@ -111,7 +130,7 @@ your browser, like Netscape 6</blink>";
else { echo "' !(protect_quote css) '"; }
?>
']
else css;;
**)
let fun patch_css (String -> String)
| [ a::_*? '
<meta
content=
"css"
/>
'; rem ] -> a @ php_css @ rem
...
...
Write
Preview
Markdown
is supported
0%
Try again
or
attach a new file
.
Attach a file
Cancel
You are about to add
0
people
to the discussion. Proceed with caution.
Finish editing this message first!
Cancel
Please
register
or
sign in
to comment