/* Desktop width. */

div#header {
  margin-bottom: 40px;
}

div.panel {
  float: left;
}
div.header2 {
  max-width: 1280px;
}
#header-title {
  margin-right: 72px;
}

.header-element {
  margin-left: 24px;
  margin-right: 24px;
  font-size: 20px;
}

a#groupsmark, a#githubmark, a#gomark {
  margin: 8px 16px;
}

img#big-logo {
  height: 216px;
}

td.side-text {
  padding-left: 64px;
  padding-right: 64px;
}

img#venn {
  height: 200px;
  padding: 8px 16px;
}

.tab-window-input,
.tab-window-output {
  float:left;
  margin: 16px 0;
}

.bigarrow {
  float: left;
  margin: 80px 8px;
  position: relative;
}

img.user-logo {
    height: 72px;
}

h1 {
  margin: 0;
}