Differences From Artifact [1f47b25d9d]:

• File src/default_css.txt — part of check-in [28b2261b75] at 2020-05-14 03:55:38 on branch fileedit-ajaxify — Minor help text, style, and layout tweaks. (user: stephan size: 22232)

To Artifact [7dc6e9ff14]:

• File src/default_css.txt — part of check-in [439f446df6] at 2020-05-14 23:34:29 on branch fileedit-ajaxify — EOL conversion: had neglected to pass that option on in the ajax request. Fixed a bug which caused duplicate CRs to get injected into force-to-windows-EOL conversions. (user: stephan size: 22251)

946
947
948
949
950
951
952

953
954
955
956
957
958
959

}
//////////////////////////////////
// Styles for /fileedit:
body.fileedit textarea {
  font-family: monospace;
  width: 100%;
  flex: 10 1 auto;

}
body.fileedit fieldset {
  margin: 0.5em 0 0.5em 0;
  padding: 0.25em 0;
  border-radius: 0.5em;
  border-color: inherit;
  border-width: 1px;

>

946
947
948
949
950
951
952
953
954
955
956
957
958
959
960

}
//////////////////////////////////
// Styles for /fileedit:
body.fileedit textarea {
  font-family: monospace;
  width: 100%;
  flex: 10 1 auto;
  height: initial;
}
body.fileedit fieldset {
  margin: 0.5em 0 0.5em 0;
  padding: 0.25em 0;
  border-radius: 0.5em;
  border-color: inherit;
  border-width: 1px;